Monday, October 26, 2015 - 3:30pm to 4:30pm
Location:Traffic 21 Classroom 6501 Gates & Hillman Centers
Speaker:JENS PALSBERG, Professor of Computer Science http://web.cs.ucla.edu/~palsberg/
For More Information, Contact:sdinardo @ cs.cmu.edu
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.
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). class="MsoNormal">In 2012 he received the ACM SIGPLAN Distinguished Service Award.