Today I talked about normalization-by-evaluation for simply typed lambda calculus.

Here are some references:

**About models for intuitionistic type theories and the notion of definitional equality**

Martin-Löf, 3rd Scandinavian Logic Symposium 1975.**An inverse of the evaluation functional for typed λ–calculus**

Berger and Schwichtenberg, LICS 1991.**Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements**

Abel, Coquand and Dybjer, LICS 2007.