Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J Scott (2001)

# Normalization by Evaluation for Typed Lambda Calculus with Coproducts

In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pp. 303-310, IEEE Computer Society (ISBN: 0-7695-1281-X).

We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based on the semantical technique known as "normalization by evaluation" and involves inverting the interpretation of the syntax into a suitable sheaf model and from this extracting appropriate unique normal forms. There is no rewriting theory involved, and the proof is completely constructive, allowing program extraction from the proof.

Document Actions