Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums

摘要

We present a notion of η -long β-normal term for the typed lambda calculus with sums and prove, using Grothendieck logical relations, that every term is equivalent to one in normal form. Based on this development we give the first type-directed partial evaluator that constructs normal forms of terms in this calculus.