[POPL'26] Stateful Differential Operators for Incremental Computing

Описание: Stateful Differential Operators for Incremental Computing (Video, POPL 2026)
Runqing Xu, Sebastian Erdweg
(KIT, Germany; KIT, Germany)

Abstract: Differential operators map input changes to output changes and form the building blocks of efficient incremental computations. For example, differential operators for relational algebra are used to perform live view maintenance in database systems. However, few differential operators are known and it is unclear how to develop and verify new efficient operators. In particular, we found that differential operators often need to use internal state to selectively cache relevant information, which is not supported by prior work. To this end, we designed a specification for \emph{stateful differential operators} that allows custom state, yet places sufficient constraints to ensure correctness. We model our specification in Rocq and show that the specification not only guides the design of novel differential operators, but also can capture some of the most sophisticated existing differential operators: database join and Datalog aggregation. We show how to describe complex incremental computations in OCaml by composing stateful differential operators, which we have extracted from Rocq.

Article: https://doi.org/10.1145/3776728

ORCID: https://orcid.org/0000-0003-1521-7379, https://orcid.org/0000-0002-1974-5956

Video Tags: Incremental computing, formal specification, doi:10.1145/3776728, orcid:0000-0003-1521-7379, orcid:0000-0002-1974-5956

Presentation at the POPL 2026 conference, Jan 11-17, 2026, https://popl26.sigplan.org/
Sponsored by ACM SIGPLAN.