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.

• Type: Conference
• Year: 2004
• Where: PPDP
• Authors: Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne
• Keywords: PPDP 2004, Raw Terms, Untyped Calculus, Untyped Term Calculus