Fri 12 Jan 2018 11:45 - 12:10 at Watercourt - Dynamic Languages Chair(s): Jean Yang

Given a tower of interpreters, i.e., a sequence of multiple interpreters interpreting one another as input programs, we aim to collapse this tower into a compiler that removes all interpretive overhead and runs in a single pass. In the real world, a use case might be Python code executed by an x86 runtime, on a CPU emulated in a JavaScript VM, running on an ARM CPU. Collapsing such a tower can not only exponentially improve runtime performance, but also enable the use of base-language tools for interpreted programs, e.g., for analysis and verification. In this paper, we lay the foundations in an idealized but realistic setting.

We present a multi-level lambda calculus that features staging constructs and stage polymorphism: based on runtime parameters, an evaluator either executes source code (thereby acting as an interpreter) or generates code (thereby acting as a compiler). We identify stage polymorphism, a programming model from the domain of high-performance program generators, as the key mechanism to make such interpreters compose in a collapsible way.

We present Pink, a meta-circular Lisp-like evaluator on top of this calculus, and demonstrate that we can collapse arbitrarily many levels of self-interpretation, including levels with semantic modi cations. We discuss several examples: compiling regular expressions through an interpreter to base code, building program transformers from modified interpreters, and others. We develop these ideas further to include re reflection and reification, culminating in Purple, a reflective language inspired by Brown, Blond, and Black, which realizes a conceptually infinite tower, where every aspect of the semantics can change dynamically. Addressing an open challenge, we show how user programs can be compiled and recompiled under user-modified semantics.

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:10
Dynamic LanguagesResearch Papers at Watercourt
Chair(s): Jean Yang Carnegie Mellon University
10:30
25m
Talk
Correctness of Speculative Optimizations with Dynamic Deoptimization
Research Papers
Olivier Flückiger Northeastern University, USA, Gabriel Scherer Northeastern University, USA, Ming-Ho Yee Northeastern University, USA, Aviral Goel Northeastern University, Amal Ahmed Northeastern University, USA, Jan Vitek Northeastern University
DOI Pre-print
10:55
25m
Talk
JaVerT: JavaScript Verification Toolchain
Research Papers
José Fragoso Santos Imperial College London, Petar Maksimović Imperial College London, Daiva Naudžiūnienė Imperial College London, Thomas Wood Imperial College London, Philippa Gardner Imperial College London
11:20
25m
Talk
Soft Contract Verification for Higher-order Stateful Programs
Research Papers
Phúc C. Nguyễn University of Maryland, Thomas Gilray University of Maryland, Sam Tobin-Hochstadt Indiana University, David Van Horn University of Maryland
11:45
25m
Talk
Collapsing Towers of Interpreters
Research Papers
Nada Amin University of Cambridge, Tiark Rompf Purdue University