Normalization by evaluation for typed lambda calculus with coproducts
Thorsten Altenkirch, Peter Dybjer, Martin O. Hofmann, Philip James Scott · 2002
Solves the decision problem for the simply typed lambda calculus with a strong binary sum, or, equivalently, the word problem for free Cartesian closed categories with binary co-products. Our method is based on the semantic technique known as "normalization by evaluation", and involves inverting the interpretation of the syntax in a suitable sheaf model and, from this, extracting an appropriate unique normal form. There is no rewriting theory involved and the proof is completely constructive, allowing program extraction from the proof.