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.
