Abstract
Typed symmetric α-calculus is a simple computational interpretation of classical logic with an involutive negation. Its main distinguishing feature is to be a true non-confluent computational interpretation of classical logic. Its non-confluence reflects the computational freedom of classical logic (as compared to intuitionistic logic). Barbanera and Berardi proved in [1],[2] that first order typed symmetric α-calculus enjoys the strong normalization property and showed in [3] that it can be used to derive symmetric programs.
In this paper we prove strong normalization for second order typed symmetric α-calculus.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
F. Barbanera, S. Berardi: A symmetric lambda-calculus for classical program extraction. Information and Computation 125 (1996) 103–117.
F. Barbanera, S. Berardi, M. Schivalocchi: “Classical” programming-with-proofsin lambda-sym: an analysis of a non-confluence. Proc. TACS’97.
M. Felleisen, D.P. Friedman, E. Kohlbecker, B. Duba: A syntactic theory of sequentialcontrol. Theoretical Computer Science 52(1987) 205–237.
M. Felleisen, R. Hieb: The revised report on the syntactic theory of sequentialcontrol and state. Theoretical Computer Science 102 (1994) 235–271.
J.Y. Girard: Linear logic. Theoretical Computer Science. 50 (1987) 1–102.
J.Y. Girard, Y. Lafont, and P. Taylor: Proofs and Types. Cambridge UniversityPress, 1989.
T. Griffin: A formulae-as-types notion of control. Proc. POPL’90 (1990) 47–58.
M. Hofmann, T. Streicher: Continuation models are universal for αμ-calculus.Proc. LICS’97 (1997) 387–397.
M. Hofmann, T. Streicher: Completeness of continuation models for αμ-calculus.Information and Computation (to appear).
M. Parigot: Free Deduction: an Analysis of “Computations” in Classical Logic.Proc. Russian Conference on Logic Programming, 1991, Springer LNCS 592 361–380.
M. Parigot: αμ-calculus: an Algorithmic Interpretation of Classical Natural Deduction.Proc. LPAR’92, Springer LNCS 624 (1992) 190–201.
M. Parigot: Strong normalization for second order classical natural deduction,Proc. LICS’93 (1993) 39–46.
M. Parigot: On the computational interpretation of negation, Proc. CSL’2000,Springer LNCS 1862 (2000) 472–484.
C.H.L. Ong, C.A. Stewart: A Curry-Howard foundation for functional computationwith control. Proc. POPL’97 (1997)
P. Selinger: Control categories and duality: on the categorical semantics of lambdamucalculus, Mathematical Structures in Computer Science (to appear).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parigot, M. (2000). Strong Normalization of Second Order Symmetric λ-Calculus. In: Kapoor, S., Prasad, S. (eds) FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2000. Lecture Notes in Computer Science, vol 1974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44450-5_36
Download citation
DOI: https://doi.org/10.1007/3-540-44450-5_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41413-1
Online ISBN: 978-3-540-44450-3
eBook Packages: Springer Book Archive