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

Vincent Balat Roberto Di Cosmo Marcelo Fiore

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


Handling properly calculi with sum types and case expressions is a difficult task as soon as one wants to take into account the commuting conversions that are so useful in performing program optimizations: there is no canonical rewriting system for calculi including such features, and performing optimization via partial evaluation was an open problem. In this paper we present a notion of canonical form for a lambda calculus with sum types, and we prove, via a sophisticated categorical construction, that any program has an equivalent canonical form. We then use ideas coming form the categorical contruction to present for the first time a type directed partial evaluator able to construct the canonical form associated to any well-typed program.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems