Sciweavers

Share
PPDP
2004
Springer

Characterizing strong normalization in a language with control operators

8 years 12 months ago
Characterizing strong normalization in a language with control operators
We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin’s λµµ. The original λµµ has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turing-complete language for computation with explicit representation of control as well as code. We define a type assignment system for the raw terms satisfying: a term is typable if and only if it is strongly normalizing. The intrinsic symmetry in the λµµ calculus leads to an essential use of both intersection and union types; in contrast to other union-types systems in the literature, our system enjoys the Subject Reduction property.
Daniel J. Dougherty, Silvia Ghilezan, Pierre Lesca
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where PPDP
Authors Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne
Comments (0)
books