Authors: Dougherty, Dan
Ghilezan, Silvia 
Lescanne, Pierre
Title: Characterizing strong normalization in a language with control operators
Journal: Proceedings of the Sixth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'04
First page: 155
Last page: 166
Conference: 6th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'04; Verona; Italy; 24 August 2004 through 26 August 2004
Issue Date: 1-Jan-2004
ISBN: 978-1-581-13819-9
We investigate some fundamental properties of the reduction relation in the untyped term alculus 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.
Keywords: Classical logic | Continuations | Functional programming | Intersection type
Publisher: Association for Computing Machinery

Show full item record


checked on May 17, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.