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
TL;DR
Mechanizes the DeCo incremental-computation calculus in Lean and proves its incrementalization transformation value-preserving (sound).
Abstract
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.
Problem
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.
Approach
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.
Results
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.