一句话：提出 DeCo 核心演算，支持泛型数据类型的静态增量函数式编程，并在 Lean 中机械化证明其可靠性。
增量计算通过避免不必要的重复计算和复用先前结果来加速程序。领域特定技术可取得显著加速，但难以泛化；通用方法则对领域特定操作支持不足，常将其视为黑盒。本文提出 DeCo，一种支持广泛用户自定义数据类型的增量函数式编程核心演算。尽管具有通用性，它能静态增量计算用户自定义数据类型上的领域特定操作，因此比其他通用技术更细粒度。作者在 Lean 中机械化该工作并证明其可靠性，即增量执行与完全重求值得到相同结果。还提供可执行实现，案例涵盖线性代数、关系代数、字典、树和无冲突复制数据类型，并对线性/关系代数及树进行了简要性能评估。
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.
@article{paperbot3817,
title = {DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types},
author = {Timon Böhler and Tobias Reinhard and David Richter and Mira Mezini},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798264}
}