Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a total universal function for the total computable functions is impossible. In this paper we break through the normalization barrier and define a self-interpreter for System F_omega, a strongly normalizing lambda-calculus. After a careful analysis of the classical theorem, we show that static type checking in F_omega excludes the proof’s diagonalization gadget and leaves open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in F_omega, including a continuation-passing style transformation. Our operations rely on a new approach to program representation that may be useful in theorem provers and compilers.
Poster (poster.pdf) | 264KiB |
Wed 20 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10 | Track 2: Types and FoundationsResearch Papers at Grand Bay South Chair(s): Robert Atkey University of Strathclyde | ||
10:30 25mTalk | Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega Research Papers Media Attached File Attached | ||
10:55 25mTalk | Type Theory in Type Theory using Quotient Inductive Types Research Papers Media Attached File Attached | ||
11:20 25mTalk | System Fω with Equirecursive Types for Datatype-generic Programming Research Papers Yufei Cai University of Tübingen, Germany, Paolo G. Giarrusso University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany Media Attached | ||
11:45 25mTalk | A Theory of Effects and Resources: Adjunction Models and Polarised Calculi Research Papers Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo Fiore Computer Laboratory, University of Cambridge, Guillaume Munch-Maccagnoni Computer Laboratory, University of Cambridge |