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. Categories and Subject Descriptors: F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages-partial evaluation; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--lambda calculus and related systems; D.3.1 [Programming Languages]: Formal Definitions and Theory--semantics General Terms: Languages, Theory, Algorithms.

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: Vincent Balat, Roberto Di Cosmo, Marcelo P. Fiore
• Keywords: Grothendieck Logical Relations, POPL 2004, Programming Languages, Theory--Semantics General Terms, Type-directed Partial Evaluator