WG211/M24Erdweg

Differential operators map input changes to output changes, which can be used to implement efficient incremental computations. For example, differential operators for relational algebra excel at supporting live view maintenance in database systems. However, there are no guidelines for developing new differential operators and there is no formal framework for proving them correct. We develop a formal framework in Coq for developing and verifying efficient differential operators. Our framework is based on a flexible theory of change structures that we present. A key novelty of our framework is that it allows differential operators to declare and use custom state, which is crucial for incremental performance. We demonstrate that our framework can be used to design new differential operators, and also model some of the most sophisticated existing operators: database join and Datalog aggregation.