ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 12:00 - 12:30 at SUN II - Security and Incremental Computation Chair(s): Zhong Shao

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 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
Security and Incremental ComputationESOP at SUN II
Chair(s): Zhong Shao Yale University
10:30
30m
Talk
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
30m
Talk
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
30m
Talk
Safe Deferred Memory Reclamation with Types
ESOP
Ismail Kuru Drexel University, Colin Gordon Drexel University
Link to publication
12:00
30m
Talk
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