Strong Normalization of Second Order Symmetric Lambda-mu Calculus

  • Yoriyuki Yamagata
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


Parigot suggested symmetric structural reduction rules for application to μ-abstraction in [9]to ensure unique representation of data type. We prove strong normalization of second order λμ-calculus with these rules.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Yuuki Andou. A normalization-procedure for the first order classical natural deduction with full symbols. Tsukuba Journal of Mathematics, 19(1):153–162, 1995.zbMATHMathSciNetGoogle Scholar
  2. 2.
    F. Barbanera and S. Berardi. A strong normalization result for classical logic. Ann. Pure Appl. Logic, 76:99–116, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    F. Barbanera and S. Berardi. A symmetric lambda calculus for “classical” program extraction. Inf. Comput., 125(2):103–117, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    V. Danos, J. B. Joinet, and H. Schellinx. A new deconstructive logic:linear logic. J. Symb. Log., 62(3):755–807, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Ph. de Groote. A cps-translation of the λμ-calculus. In Trees in algebra and programming, CAAP’ 94, number 787 in Lect. Notes Comput. Sci, pages 85–99. Springer-Verlag, 1994.Google Scholar
  6. 6.
    Ph. de Groote. On the relation between λμ-calculus and the syntactic theory of sequential control. In Logic programming and automated reasoning, volume 822 of Lect. Notes Comput. Sci, pages 31–43. Springer-Verlag, 1994.Google Scholar
  7. 7.
    C.-H. L. Ong and C. A. Stewart. A curry-howard foundation for functional computation with control. In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM press, January 1997.Google Scholar
  8. 8.
    M. Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Artificial Intelligence, pages 190–201. Springer-Verlag, 1992.Google Scholar
  9. 9.
    M. Parigot. Classical proofs as programs. In Computational logic and proof theory, volume 713 of Lect. Notes Comput. Sci, pages 263–276. Springer-Verlag, 1993.CrossRefMathSciNetGoogle Scholar
  10. 10.
    M. Parigot. Strong normalization for second order classical natural deduction. J. Symb. Log., 62(4):1461–1479, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    M. Parigot. On the computational interpretation of negation. In P. Clote and H. Schwichtenberg, editors, Computer Science Logic, volume 1862 of Lect. Notes Comput. Sci, pages 472–484. Springer-Verlag, 2000.Google Scholar
  12. 12.
    Th. Streicher and B. Reus. Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6):543–572, 1998.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Yoriyuki Yamagata

There are no affiliations available

Personalised recommendations