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.