% Incremental λ-Calculus % Paolo G. Giarrusso
This is the homepage for the Incremental λ-Calculus project. Our goal is to extend database technology for low-overhead incremental computation, based on finite differencing, and apply it to higher-order languages.
-
Incremental λ-Calculus in Cache-Transfer Style --- Static Memoization by Program Transformation. Paolo G. Giarrusso, Yann Régis-Gianas and Philipp Schuster. ESOP 2019. Supersedes Chapter 17 of Giarrusso's PhD thesis.
- Extended version.
- Supplementary material: Implementation and Coq formalization.
-
A theory of changes for higher-order languages — incrementalizing λ-calculi by static differentiation (updated version). Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel and Klaus Ostermann. PLDI 2014, pp. 145--155.
-
Optimizing and Incrementalizing Higher-order Collection Queries by AST Transformation. Paolo G. Giarrusso's PhD thesis. Some highlights:
- A novel, simpler correctness proof for ILC on simply-typed λ-calculus, where validity is captured by a logical relation (Ch. 12-13-14).
- A reformulation of that proof using (step-indexed) logical relations and operational semantics, for simply-typed λ-calculus (without or with recursion) and untyped λ-calculus (Appendix C).
- Chapter 17 is superseded by the extended version of the ESOP'19 paper.
- Agda machine-checked proofs --- inc-lc/ilc-agda/Thesis, for Ch. 12-14.
By other authors:
- Seminaïve evaluation for a higher-order functional language. Michael Arntzenius and Neel Krishnaswami. POPL 2020.
This project benefited from code and ideas of many different people:
- Cai Yufei
- Paolo G. Giarrusso
- Tillmann Rendel
- Klaus Ostermann
- Lourdes Del Carmen Gonzàlez Huesca
- Yann Régis-Gianas
- Philipp Schuster
Further acknowledgments in each publication.
- 2020-01-23: Updated version of this page and of Giarrusso's PhD thesis.
- 2015-03-16: [Slides of the Paris talk online](resources/2015-01-22 ILC Paris.pdf).
- 2015-01-22: Talk about ILC project at the Paris Diderot (Paris 7) University.
- 2014-06-07: Sources online on GitHub --- see inc-lc/ilc-scala and inc-lc/ilc-agda.
- 2014-05-04: Author's version of the paper camera-ready finally online.
- 2014-03-15: The AEC submission was found to "meet or exceed expectations"!
- 2014-02-21: Link to the AEC submission.
- 2014-02-10: Submission to the artifact evaluation committee (AEC) evaluation
- 2014-02-05: Website online
- 2014-02-03: Our first paper on this project was accepted for PLDI '14! The author's version of the camera-ready is available.
For any question or suggestion, feel free to contact me, Paolo G. Giarrusso, at p !dot! giarrusso (at) gmail !dot! com.