Search papers, labs, and topics across Lattice.
The paper introduces DeCo, a core calculus designed for incremental functional programming that supports user-defined data types and domain-specific operations. DeCo achieves static incrementalization of these operations, offering finer-grained control than black-box approaches and enabling efficient reuse of previous results. The authors formalized DeCo in Lean, proving its soundness, and demonstrated its applicability through case studies and performance evaluations across domains like linear algebra, relational algebra, and tree processing.
DeCo achieves fine-grained static incrementalization of domain-specific operations on user-defined data types, outperforming generic black-box approaches.
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.
