## 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**.