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
Times are displayed in time zone: Tijuana, Baja California change

13:40 - 15:20
Interpretation and EvaluationResearch Papers at Watercourt
Chair(s): Atsushi IgarashiKyoto University, Japan
13:40
25m
Talk
Unifying Analytic and Statically-Typed Quasiquotes
Research Papers
Lionel ParreauxEPFL, Antoine VoizardUniversity of Pennsylvannia, Amir ShaikhhaEPFL, Christoph E. KochEPFL
Pre-print
14:05
25m
Talk
Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Research Papers
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles (UCLA)
14:30
25m
Talk
Migrating Gradual Types
Research Papers
John Peter CamporaULL Lafayette, Sheng ChenUniversity of Louisiana at Lafayette, Martin ErwigOregon State University, Eric WalkingshawOregon State University
14:55
25m
Talk
Intrinsically-Typed Definitional Interpreters for Imperative Languages
Research Papers
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