Professor of Computer Science, UCLA
Breaking Through the Normalization Barrier
According to conventional wisdom, a self-interpreter for a strongly normalizing lambda-calculus is impossible.
We call this the normalization barrier.
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
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
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.
Jens Palsberg is a Professor of Computer Science at University of California, Los Angeles (UCLA).
research interests span the areas of compilers, embedded systems,
programming languages, software engineering, and information security.
He is the editor-in-chief of
Transactions of Programming Languages and Systems, and a former
conference program chair of ACM Symposium on Principles of Programming
In 2012 he received the ACM SIGPLAN Distinguished Service Award.
Monday, October 26, 2015
& Hillman Centers 6501
of Programming Seminars