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 JanDisplayed time zone: Tijuana, Baja California change
10:30 - 12:10 | |||
10:30 25mTalk | 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 25mTalk | 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 25mTalk | 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 25mTalk | Collapsing Towers of Interpreters Research Papers |