A Framework of Differential Operators
summary
A Coq formalization presents a reusable framework that defines change structures (value, delta, patch, valid-change relation) and proves correctness of stateless and stateful differential operators by requiring valid input changes and an invertible change structures condition. It verifies several existing operators and derives new ones, models sum as O(1) on insertion, shows trim_right needs two small states (count and all-space flag), and encodes join-index and aggregation-tree implementations with sequential-correctness proofs.
AI-written summary · about
chapters (9)
- 0:00Verified differential operators
- 1:49Incremental computing approaches
- 6:25Limitations and framework goals
- 7:28Change structures and invertibility
- 10:17Stateless operators interface
- 12:43Exercise: trim right operator
- 15:55Stateful operators and state changes
- 18:04Case studies and future work
- 19:12Q&A
related talks
27mProvably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic
13mFormalizing a First-order Differentiable Logic with MathComp
15mSafe Couplings: Coupled Refinement Types
01h 03mInside Every Calculus Is A Little Algebra Waiting To Get Out
36mProgramming Languages for Automatic Differentiation: What Now?
55mProving Theorems and Certifying Programs with Coq
59mDifferential Verification of Deep Neural Networks
30mλS: Computable Semantics for Diff'ble Programming with HO Functions and Datatypes