← All papers
First page of DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types

DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types

Timon Böhler, Tobias Reinhard, David Richter, Mira Mezini

cs.PL Feb 24, 2026 · v1
Mechanizes the DeCo incremental-computation calculus in Lean and proves its incrementalization transformation value-preserving (sound).
Incrementalization speeds up computations by avoiding unnecessary recomputations and by efficiently reusing previous results. While domain-specific techniques achieve impressive speedups, e.g., in the context of database queries, they are difficult to generalize. Meanwhile, general approaches offer little support for incrementalizing domain-specific operations. In this work, we present DeCo, a novel core calculus for incremental functional programming with support for a wide range of user-defined data types. Despite its generic nature, our approach statically incrementalizes domain-specific operations on user-defined data types. It is, hence, more fine-grained than other generic techniques which resort to treating domain-specific operations as black boxes. We mechanized our work in Lean and proved it sound, meaning incrementalized execution computes the same result as full reevaluation. We also provide an executable implementation with case studies featuring examples from linear algebra, relational algebra, dictionaries, trees, and conflict-free replicated data types, plus a brief performance evaluation on linear and relational algebra and on trees.

Incrementalization speeds up computations by reusing previous results, but general approaches offer little support for domain-specific operations, while domain-specific techniques are hard to generalize. Existing generic approaches treat domain-specific operations as black boxes.

DeCo is a core calculus for incremental functional programming that supports a wide range of user-defined data types. It statically incrementalizes domain-specific operations on user-defined data types at a finer granularity than other generic techniques. The work is mechanized in Lean with a soundness proof showing that incrementalized execution computes the same result as full reevaluation. An executable implementation includes case studies in linear algebra, relational algebra, dictionaries, trees, and CRDTs.

The soundness theorem is proved in Lean, guaranteeing that incremental updates produce identical results to full recomputation. Performance evaluation on linear and relational algebra and trees demonstrates practical speedups from the fine-grained incremental approach.