Professor of Computer Science, UCLA

Breaking Through the Normalization Barrier

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.

Principles
of Programming Seminars