Incremental λ-Calculus in Cache-Transfer Style, Static Memoization by Program Transformation
Incremental computation requires propagating changes and reusing intermediate results of base computations. Derivatives, as produced by static differentiation, propagate changes but do not reuse intermediate results, leading to wasteful recomputation. As a solution, we introduce conversion to Cache-Transfer-Style, an additional program transformations producing purely incremental functional programs that create and maintain nested tuples of intermediate results. To prove CTS conversion correct, we extend the correctness proof of static differentiation from STLC to untyped $\lambda$-calculus via step-indexed logical relations, and prove sound the additional transformation via simulation theorems. To show ILC-based languages can improve performance relative to from-scratch recomputation, and that CTS conversion can extend its applicability, we perform an initial performance case study. We provide derivatives of primitives for operations on collections and incrementalize selected example programs using those primitives, confirming expected asymptotic speedups.
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | |||
10:30 30mTalk | Robustly Safe Compilation ESOP Marco Patrignani Stanford University & CISPA Helmholtz Center for Information Security, Deepak Garg Max Planck Institute for Software Systems Link to publication | ||
11:00 30mTalk | Compiling Sandboxes: Formally Verified Software Fault Isolation ESOP Frédéric Besson , Sandrine Blazy Univ Rennes- IRISA, Alexandre Dang , Thomas P. Jensen INRIA Rennes, Pierre Wilke Yale University Link to publication | ||
11:30 30mTalk | Safe Deferred Memory Reclamation with Types ESOP Link to publication | ||
12:00 30mTalk | Incremental λ-Calculus in Cache-Transfer Style, Static Memoization by Program Transformation ESOP Paolo G. Giarrusso TU Delft, The Netherlands, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Philipp Schuster University of Tübingen, Germany Link to publication |