Write a Blog >>
Wed 20 Jan 2016 10:30 - 10:55 at Grand Bay South - Track 2: Types and Foundations Chair(s): Robert Atkey

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 Jan

10:30 - 12:10: Research Papers - Track 2: Types and Foundations at Grand Bay South
Chair(s): Robert AtkeyUniversity of Strathclyde
POPL-2016-papers10:30 - 10:55
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles
Media Attached File Attached
POPL-2016-papers10:55 - 11:20
Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham
Media Attached File Attached
POPL-2016-papers11:20 - 11:45
Yufei CaiUniversity of Tübingen, Germany, Paolo G. GiarrussoUniversity of Tübingen, Germany, Klaus OstermannUniversity of Tübingen, Germany
Media Attached
POPL-2016-papers11:45 - 12:10
Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt, Marcelo FioreComputer Laboratory, University of Cambridge, Guillaume Munch-MaccagnoniComputer Laboratory, University of Cambridge