Sciweavers

Share
POPL
2016
ACM

Breaking through the normalization barrier: a self-interpreter for f-omega

1 years 5 months ago
Breaking through the normalization barrier: a self-interpreter for f-omega
According to conventional wisdom, a self-interpreter for a strongly normalizing λ-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ω, a strongly normalizing λ-calculus. After a careful analysis of the classical theorem, we show that static type checking in Fω can exclude the proof’s diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in Fω, 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. Categories and Subject Descriptors D.3.4 [Processors]: Interpreters; D.2.4 [Program Verification]: Correctnes...
Matt Brown, Jens Palsberg
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Matt Brown, Jens Palsberg
Comments (0)
books