一句话：提出有状态差分算子的形式规约，在 Rocq 中机械化验证，可指导新算子设计并刻画 join 与 Datalog 聚合等既有算子。
差分算子把输入变化映射为输出变化，是高效增量计算的基本构件，例如关系代数差分算子被用于数据库的实时视图维护。然而已知的差分算子种类很少，且如何开发并验证新的高效算子尚不明确；作者发现差分算子常需借助内部状态来有选择地缓存相关信息，而既有工作并不支持这一点。为此，论文为有状态差分算子设计了一套规约：既允许算子自定义状态，又施加足够约束以保证正确性。作者在 Rocq 中对规约建模并机械化验证，表明该规约既能指导新差分算子的设计，也能刻画一些最复杂的既有差分算子，如数据库 join 与 Datalog 聚合。最后，作者从 Rocq 提取实现到 OCaml，通过组合有状态差分算子来描述复杂的增量计算。
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 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{XuE26,
title = {Stateful Differential Operators for Incremental Computing},
author = {Runqing Xu and Sebastian Erdweg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776728}
}