skip to main content
10.1145/1013963.1013982acmconferencesArticle/Chapter ViewAbstractPublication PagesppdpConference Proceedingsconference-collections
Article

Characterizing strong normalization in a language with control operators

Published: 24 August 2004 Publication History

Abstract

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.

References

[1]
Z. M. Ariola and H. Herbelin. Minimal classical logic and control operators. In ICALP: Annual International Colloquium on Automata, Languages and Programming, volume 2719 of Lecture Notes in Computer Science, pages 871--885. sv, 2003.]]
[2]
F. Barbanera and S. Berardi. A symmetric lambda calculus for classical program extraction. Information and Computation, 125(2):103--117, 1996.]]
[3]
F. Barbanera, M. Dezani-Ciancaglini, and U. de' Liguoro. Intersection and union types: syntax and semantics. Information and Computation, 119(2):202--230, 1995.]]
[4]
H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931--940 (1984), 1983.]]
[5]
H. P. Barendregt and S. Ghilezan. Lambda terms for natural deduction, sequent calculus and cut-elimination. Journal of Functional Programming, 10(1):121--134, 2000.]]
[6]
G. M. Bierman. A computational interpretation of the λμ-calculus. In Proceedings of Symposium on Mathematical Foundations of Computer Science., volume 1450 of Lecture Notes in Computer Science, pages 336--345. Springer-Verlag, 1998.]]
[7]
P. Buneman and B. Pierce. Union types for semistructured data. In Internet Programming Languages, volume 1686 of Lecture Notes in Computer Science. Springer-Verlag, September 1998. Proceedings of the International Database Programming Languages Workshop.]]
[8]
M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and λ-calculus semantics. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 535--560. Academic Press, London, 1980.]]
[9]
P.-L. Curien. Symmetry and interactivity in programming. Archive for Mathematical Logic, 2001. to appear.]]
[10]
P.-L. Curien. Abstract machines, control, and sequents. In Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, volume 2395 of Lecture Notes in Computer Science, pages 123--136. Springer-Verlag, 2002.]]
[11]
P.-L. Curien and H. Herbelin. The duality of computation. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montreal, Canada, 2000. ACM Press.]]
[12]
R. David. Normalization without reducibility. Annals of Pure and Applied Logic, 107:121--130, 2001.]]
[13]
Ph. de Groote. On the relation between the λμ-calculus and the syntactic theory of sequential control. In Springer-Verlag, editor, Proceedings of the (th International Conference on Logic Programming and Automated Reasoning, (LPAR'94), volume 822 of Lecture Notes in Computer Science, pages 31--43, 1994.]]
[14]
J.-Y. Girard. A new constrcutive logic: classical logic. Mathematical Structures in Computer Science, 1(3):255--296, 1991.]]
[15]
T. Griffin. A formulae-as-types notion of control. In Proceedings of the 17th Annual ACM Symposium on Principles Of Programming Languages, Orlando (Fla., USA), pages 47--58, 1990.]]
[16]
H. Herbelin. Séquents qu'on calcule~: de l'interprétation du calcul des séquents comme calcul de λ-termes et comme calcul de stratégies gagnantes. Thèse d'université, Université Paris 7, Janvier 1995.]]
[17]
J. R. Hindley. Coppo--Dezani types do not correspond to propositional logic. Theoretical Computer Science, 28(1-2):235--236, 1984.]]
[18]
O. Laurent. On the denotational semantics of the pure lambda-mu calculus. Manuscript, 2004.]]
[19]
S. Lengrand. Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In Bernhard Gramlich and Salvador Lucas, editors, Electronic Notes in Theoretical Computer Science, volume 86. Elsevier, 2003.]]
[20]
C.-H. L. Ong and C. A. Stewart. A Curry-Howard foundation for functional computation with control. In Proceedings of the 24th Annual ACM Symposium on Principles Of Programming Languages, Paris (France), pages 215--227, 1997.]]
[21]
J. Palsberg and C. Pavlopoulou. From polyvariant flow information to intersection and union types. J. Funct. Programming, 11(3):263--317, 2001.]]
[22]
M. Parigot. An algorithmic interpretation of classical natural deduction. In Proc. of Int. Conf. on Logic Programming and Automated Reasoning, LPAR'92, volume 624 of Lecture Notes in Computer Science, pages 190--201. Springer-Verlag, 1992.]]
[23]
M. Parigot. Proofs of strong normalisation for second order classical natural deduction. The Journal of Symbolic Logic, 62(4):1461--1479, December 1997.]]
[24]
B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, February 1991.]]
[25]
E. Polonovski. Strong normalization of λμμ-calculus with explicit substitutions. In Igor Walukiewicz, editor, Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, volume 2987 of Lecture Notes in Computer Science, pages 423--437. Springer, 2004.]]
[26]
G. Pottinger. Normalization as homomorphic image of cut-elimination. Annals of Mathematical Logic, 12:323--357, 1977.]]
[27]
G. Pottinger. A type assignment for the strongly normalizable λ-terms. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 561--577. Academic Press, London, 1980.]]
[28]
J. C. Reynolds. Design of the programming language Forsythe. Report CMU--CS--96--146, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 28, 1996.]]
[29]
C. Urban and G. M. Bierman. Strong normalisation of cut-elimination in classical logic. In Typed Lambda Calculus and Applications, volume 1581 of Lecture Notes in Computer Science, pages 365--380, 1999.]]
[30]
P. Wadler. Call-by-value is dual to call-by-name. In Proceedings of the 8th International Conference on Functional Programming, 2003.]]
[31]
J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Programming, 12(3):183--227, May 2002.]]

Cited By

View all
  • (2019) Characterizing of Strong Normalization for Λμ -Calculus Journal of Physics: Conference Series10.1088/1742-6596/1187/4/0420461187:4(042046)Online publication date: 8-May-2019
  • (2017)Characterization of strong normalizability for a sequent lambda calculus with co-controlProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131867(163-174)Online publication date: 9-Oct-2017
  • (2014)A Translation of Intersection and Union Types for the λμ-CalculusProgramming Languages and Systems10.1007/978-3-319-12736-1_7(120-139)Online publication date: 2014
  • Show More Cited By

Index Terms

  1. Characterizing strong normalization in a language with control operators

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM Conferences
      PPDP '04: Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming
      August 2004
      260 pages
      ISBN:1581138199
      DOI:10.1145/1013963
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Sponsors

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 24 August 2004

      Permissions

      Request permissions for this article.

      Check for updates

      Author Tags

      1. classical logic
      2. continuations
      3. functional programming
      4. intersection type

      Qualifiers

      • Article

      Conference

      PPDP04
      Sponsor:

      Acceptance Rates

      Overall Acceptance Rate 230 of 486 submissions, 47%

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)2
      • Downloads (Last 6 weeks)0
      Reflects downloads up to 27 Jan 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2019) Characterizing of Strong Normalization for Λμ -Calculus Journal of Physics: Conference Series10.1088/1742-6596/1187/4/0420461187:4(042046)Online publication date: 8-May-2019
      • (2017)Characterization of strong normalizability for a sequent lambda calculus with co-controlProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131867(163-174)Online publication date: 9-Oct-2017
      • (2014)A Translation of Intersection and Union Types for the λμ-CalculusProgramming Languages and Systems10.1007/978-3-319-12736-1_7(120-139)Online publication date: 2014
      • (2008)Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculusTheoretical Computer Science10.1016/j.tcs.2008.01.022398:1-3(114-128)Online publication date: 20-May-2008
      • (2007)Simple proofs of characterizing strong normalization for explicit substitution calculiProceedings of the 18th international conference on Term rewriting and applications10.5555/1779782.1779802(257-272)Online publication date: 26-Jun-2007
      • (2007)Simple Proofs of Characterizing Strong Normalization for Explicit Substitution CalculiTerm Rewriting and Applications10.1007/978-3-540-73449-9_20(257-272)Online publication date: 2007
      • (2006)Structure of proofs and the complexity of cut eliminationTheoretical Computer Science10.1016/j.tcs.2005.07.042353:1(63-70)Online publication date: 14-Mar-2006
      • (2005)Intersection and Union Types in the λμμ~-calculusElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.06.010136(153-172)Online publication date: 1-Jul-2005
      • (2005)Intersection and Union Types for XElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.06.009136(203-227)Online publication date: 1-Jul-2005
      • (2005)λµ-calculus and dualityProceedings of the 16th international conference on Term Rewriting and Applications10.1007/978-3-540-32033-3_16(204-218)Online publication date: 19-Apr-2005
      • Show More Cited By

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media