Normalization by Evaluation

Lecturer: Prof. Peter Dybjer (Chalmers University of Technology, Sweden).

About the lecturer | Abstract | Slides | Assignment

About the lecturer: Peter Dybjer is professor of computing science at Chalmers University of Technology in Gothenburg, Sweden. He got his MSc at UCLA in 1980, was a visiting PhD student at the University of Edinburgh 1980-81, and received his PhD at Chalmers in 1983. He has been a guest researcher at the Newton Institute for Mathematical Sciences in Cambridge, England and at the Mittag-Leffler Institute in Djursholm, Sweden. He was the founder of the EU working group on Applied Semantics, and has also participated in the EU projects on Categorical Logic in Computer Science and Types for Proofs and Programs. Peter Dybjer is an invited speaker at various scientific meetings (e.g. MFPS 2008) and is going to give a keynote talk at FLOPS 2008.
His main interests revolve around Martin-L÷f's constructive type theory. He has in particular contributed to the constructive theory of inductive definitions, and found the new unifying principle of "inductive-recursive definition" which helps systematizing the constructive higher infinite. Other interests include interactive proof assistants, semantics of programming languages, the connection between category theory and type theory, and normalization by evaluation.

Course summary: Normalization by evaluation is a new method for writing normalization algorithms. The idea is to first build a data structure which represents a model of the language in question. Then terms are interpreted in this model, and finally the normal forms are extracted from the semantic values. The method has both practical and theoretical interest. It has been used for program simplification (type-directed partial evaluation) and in type-checking algorithms for proof assistants based on type theory. Ideas from several fields in theoretical computer science are useful for analyzing the method, such as constructive type theory and program extraction, category theory, and domain theory. These lectures will both give an introduction to the technique and discuss some of these connections.

Lecture slides [PDF]

Assignment: [PDF] due March 31, 2008.
Please send your solutions in PDF by e-mail to peterd AT cs DOT chalmers DOT se.