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 :
Reports
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101950
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:10:35 AM
Last modification on : Wednesday, November 20, 2019 - 2:53:00 AM

File

RR2004-29.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101950, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

15

Files downloads

45