Wed 10 Jan 2018 14:05 - 14:30 at Watercourt - Interpretation and Evaluation Chair(s): Atsushi Igarashi

We present partial evaluation by specialization-safe normalization, a novel partial evaluation technique that is Jones-optimal, that can be self-applied to achieve the Futamura projections and that can be type-checked to ensure it always generates code with the correct type. Jones-optimality is the gold-standard for nontrivial partial evaluation and guarantees that a specializer can remove an entire layer of interpretation. We achieve Jones-optimality by using a novel affine-variable static analysis that directs specialization-safe normalization to always decrease a program’s runtime.

We demonstrate the robustness of our approach by showing Jones-optimality in a variety of settings. We have formally proved that our partial evaluator is Jones-optimal for call-by-value reduction, and we have experimentally shown that it is Jones-optimal for call-by-value, normal-order, and memoized normal-order. Each of our experiments tests Jones-optimality with three different self-interpreters.

We implemented our partial evaluator in F$_\omega^{\mu i}$, a recent language for typed self-applicable meta-programming. It is the first Jones-optimal and self-applicable partial evaluator whose type guarantees that it always generates type-correct code.

Wed 10 Jan

13:40 - 15:20: Research Papers - Interpretation and Evaluation at Watercourt
Chair(s): Atsushi IgarashiKyoto University, Japan
POPL-2018-papers13:40 - 14:05
Lionel ParreauxEPFL, Antoine VoizardUniversity of Pennsylvannia, Amir ShaikhhaEPFL, Christoph E. KochEPFL
POPL-2018-papers14:05 - 14:30
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles (UCLA)
POPL-2018-papers14:30 - 14:55
John Peter Campora IIIULL Lafayette, Sheng ChenUniversity of Louisiana at Lafayette, Martin ErwigOregon State University, Eric WalkingshawOregon State University
POPL-2018-papers14:55 - 15:20
Casper Bach PoulsenDelft University of Technology, Arjen RouvoetDelft University of Technology, Andrew TolmachPortland State University, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
DOI Pre-print