Skip to Main content Skip to Navigation

Characterizing strong normalization in a language with control operators.

Abstract : We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin's lambda-mu-mu~. The original lambda-mu-mu~ 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 lambda-mu-mu~ 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.
Document type :
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:10:35 AM
Last modification on : Wednesday, November 20, 2019 - 2:53:00 AM


Files produced by the author(s)


  • HAL Id : hal-02101950, version 1



Dan Dougherty, Silvia Ghilezan, Pierre Lescanne. Characterizing strong normalization in a language with control operators.. [Research Report] LIP RR-2004-29, Laboratoire de l'informatique du parallélisme. 2004, 2+26p. ⟨hal-02101950⟩



Record views


Files downloads