Stateful Differential Operators for Incremental Computing
summary
Presents a formal specification for stateful differential operators that lets operators store and update custom state, proves correctness in Rocq, and extracts executable code to OCaml extraction. Models include database join and Datalog aggregation and several novel string operators; correctness uses patch-based change structures and commutative diagrams. Benchmarks from the extracted implementation show consistent incremental speedups versus full recomputation and demonstrate practical gains, though no direct comparison to systems like Differential Dataflow is provided.
AI-written summary · about
chapters (12)
- 0:00Incremental computing intro
- 1:24Two approaches in incremental computing
- 4:58Differential vs selective recomputation
- 9:32Limitations of differential operators
- 10:15Formal framework for operators
- 13:47Verifying correctness
- 16:58Stateful operators explained
- 19:06Formal spec of operators
- 20:12Case studies and operators
- 21:58Benchmarking incremental operators
- 23:23Conclusion and future work
- 23:43Q&A
related talks
36mData Driven UIs, Incrementally
15mIncremental Processing of Structured Data in Datalog
01h 01mLogic and Algebras for Distributed Computing: Applications and Open Questions
32mReactive Datalog for Datomic
17mBetter Together: Unifying Datalog and Equality Saturation
33mA (Semi)Ring-Based Query Algebra for Incremental View Maintenance and Query Compilation
01h 01mDatalog and Equality Saturation
17mA Systematic Approach to Deriving Incremental Type Checkers