Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
bd95e61
Add reactive view example catalogue and research scaffolding
cristianoc Dec 1, 2025
3e41076
Add DCE formalization and clarify reduce semantics
cristianoc Dec 1, 2025
83f6d15
Document reducer calculus and layer-2 non-reducer analysis
cristianoc Dec 1, 2025
32d5eaf
Expand reactive calculus notes with JSON ordering, add test harnesses
cristianoc Dec 2, 2025
430d9a3
Add examples primitives analysis with detailed deep dives
cristianoc Dec 2, 2025
857a774
fix example 6.3
cristianoc Dec 2, 2025
3c6bbf9
Clarify DBToaster equivalence claims in examples analysis
cristianoc Dec 2, 2025
b51c3de
Move DBToaster discussion to Example 6.3 (Yannakakis joins)
cristianoc Dec 2, 2025
b5458b1
Split Lean DCE Layer2 and align TeX with reactive/incremental split
cristianoc Dec 3, 2025
7a3ea68
Clarify incremental DCE correctness invariant
cristianoc Dec 3, 2025
9b13fa3
Add research note: Incremental Fixpoint Computation - Two-Level Archi…
cristianoc Dec 3, 2025
48e4b96
Add Level 1 formalization: IncrementalFixpoint.lean
cristianoc Dec 3, 2025
4db0301
Formalize counting-based cascade algorithm and overall correctness
cristianoc Dec 3, 2025
3954bb4
Add well-founded derivations for contraction completeness
cristianoc Dec 3, 2025
12a0462
Complete well-founded cascade proofs
cristianoc Dec 3, 2025
562febb
Add helper lemmas for semi-naive expansion proof
cristianoc Dec 3, 2025
69d8418
Clean up: remove unused definitions and lemmas from Lean and TeX
cristianoc Dec 3, 2025
f9d01f9
Complete all Lean proofs - no more sorry
cristianoc Dec 3, 2025
5bd297a
Add implementable API with explicit ranks and concrete pseudo-code
cristianoc Dec 3, 2025
a4cfb2b
Clean up Level 1 API section with clear structure
cristianoc Dec 3, 2025
28e44ad
Simplify API: make stepInv optional, document two API levels
cristianoc Dec 3, 2025
6b289f8
detailed DCE example
cristianoc Dec 3, 2025
d670a7c
Add incremental fixpoint combinator with two-level API
cristianoc Dec 3, 2025
2d556a9
Fix Js.typeof deprecation warnings and minor whitespace
cristianoc Dec 3, 2025
7260995
Simplify dce_reactive_view.tex to reference generic fixpoint
cristianoc Dec 3, 2025
d5584e3
Add Datalog/database references to incremental fixpoint notes
cristianoc Dec 4, 2025
19c09ba
Refactor Fixpoint to use native JS collections and fix stale ranks bug
cristianoc Dec 4, 2025
dc67126
Update AGENTS.md
cristianoc Dec 5, 2025
c7673df
Fix linter warnings in IncrementalFixpoint.lean
cristianoc Dec 8, 2025
68af0e6
Add concrete anti-join examples to paper and analysis
cristianoc Dec 8, 2025
2d886b5
Update REACTIVE_CALCULUS_NOTES.md: clarify local vs global calculi
cristianoc Dec 8, 2025
25ce807
Add anti-join examples and refine example classifications
cristianoc Dec 8, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,9 @@ lib/
*.cmj
*.cmi
*.rei
reduce.aux
reduce.log

# LaTeX build artifacts
*.aux
*.log
*.toc
*.out
8 changes: 8 additions & 0 deletions AGENTS.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
This repo uses ReScript `.res` files alongside TypeScript and other sources.

Style and syntax guidelines:

- For ReScript array literals, always use the JavaScript/TypeScript-style syntax `[...]` (for example, `[1, 2, 3]`), **not** the Reason/OCaml-style `[| ... |]`.
- When adding or editing ReScript code, follow the existing style in nearby modules unless explicitly overridden here.
- Prefer the stdlib names actually available in this codebase: use `min` instead of `Int.min`, `List.toArray` instead of `Array.of_list`, and build arrays with loops or lists (then `List.toArray`) instead of `Array.init`.
- When discarding a value, pipe to `ignore` (e.g. `expr->ignore`) rather than using `let _ = expr`.
Loading