Sciweavers

POPL
2004
ACM

Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

14 years 10 months ago
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.
Vincent Balat, Roberto Di Cosmo, Marcelo P. Fiore
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2004
Where POPL
Authors Vincent Balat, Roberto Di Cosmo, Marcelo P. Fiore
Comments (0)