Abstract:
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. I will show how to break through the normalization
barrier and define a self-interpreter for a widely used strongly
normalizing lambda-calculus. After a careful analysis of the
classical theorem, we show that static type checking can exclude the
proof's diagonalization gadget and leave open the possibility for a
self-interpreter. Our self-interpreter relies on a novel program representation that may be useful in theorem provers and compilers. Joint work with Matt Brown, to be presented at POPL 2016.
Bio: Jens Palsberg is a Professor of Computer Science at University of California, Los Angeles (UCLA). His
research interests span the areas of compilers, embedded systems,
programming languages, software engineering, and information security. He is the editor-in-chief of ACM
Transactions of Programming Languages and Systems, and a former
conference program chair of ACM Symposium on Principles of Programming
Languages (POPL). In 2012 he received the ACM SIGPLAN Distinguished Service Award.