DIKU ITU

Copenhagen Programming Language Seminar

COPLAS Talk

Normalization by Evaluation for Dependent Types

Peter Dybjer,
Chalmers University, Gothenburg

Thursday, February 22nd, Time: 15:00 - 16:00 (!)
IT University of Copenhagen, Rued Langgaards Vej 7, auditorium 3

Abstract:

Normalization by evaluation is a technique for writing programs which normalize terms in various languages. This technique was first introduced by Martin-Löf in 1973 for proving normalization for the first version of his constructive type theory. It arose an application of his ideas about constructive model theory: to constructively prove that each term has a normal form is the same thing as writing a program which returns this normal form (together with a construction which shows that it is indeed a normal form).

The 1973 version of type theory was a combinatory theory with a weak notion of reduction. It was later abandonded and replaced by type theories based on the lambda calculus with beta and eta conversion. In 1991 Berger and Schwichtenberg rediscovered the normalization by evaluation technique and used it to compute long beta-eta normal forms in the simply typed lambda calculus. Normalization by evaluation gives a fresh view of normalization problems, and Berger and Schwichtenberg's work gave rise to a lot of activity, such as generalizations to numerous different languages, applications in partial evaluation, formalizations in proof assistants, and connections with category theory. However, in spite of the fact that the technique was discovered for constructive type theory, it is only recently that the technique has been considered for the modern versions of constructive type theory and other systems with dependent types. In this talk I will give an introduction to some recent joint work together with Andreas Abel, Klaus Aehlig, and Thierry Coquand which shows how to do normalization by evaluation for dependent types based on ideas for how to do normalization by evaluation for the untyped lambda calculus.

Scientific host: Carsten Schüermann. Administrative host: Camilla Torp-Smith. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org