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.