Normalization by Evaluation for Typed Lambda Calculus with Coproducts.

Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott

Browse the full LICS paper archive.