DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Tue 6 OctDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 17:00 | Refinement Types and Functional ProgrammingOOPSLA at East Hall 2 Chair(s): Nadia Polikarpova University of California at San Diego | ||
15:30 18mTalk | PLEX: Normalization for Refinement Types OOPSLA Alessio Ferrarini IMDEA Software Institute; Universidad Politécnica de Madrid, Niki Vazou IMDEA Software Institute, Wouter Swierstra Utrecht University Link to publication DOI | ||
15:48 18mTalk | First-Class Refinement Types for Scala OOPSLA DOI Pre-print | ||
16:06 18mTalk | Effectively Propositional Higher-Order Functional Programming OOPSLA Nicholas V. Lewchenko University of Colorado Boulder, Kunha Kim University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder; Amazon, Gowtham Kaki University of Colorado Boulder DOI | ||
16:24 18mTalk | DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types OOPSLA Timon Böhler TU Darmstadt, Tobias Reinhard TU Darmstadt, David Richter TU Darmstadt, Mira Mezini Technische Universität Darmstadt; ATHENE; hessian.AI DOI Pre-print | ||