Hereditary substitution for the \(\lambda \Delta \)-calculus. (English) Zbl 1471.03023
de’Liguoro, Ugo (ed.) et al., Proceedings of the first workshop on control operators and their semantics, COS 2013, Eindhoven, The Netherlands, June 24–25, 2013. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 127, 45-65 (2013).
Summary: Hereditary substitution is a form of type-bounded iterated substitution, first made explicit by K. Watkins et al. [Lect. Notes Comput. Sci. 3085, 355–377 (2004; Zbl 1100.68548)] and
R. Adams [Lect. Notes Comput. Sci. 3085, 1–16 (2004; Zbl 1100.68542)]
in order to show normalization of proof terms for various constructive logics. This paper is the first to apply hereditary substitution to show normalization of a type theory corresponding to a non-constructive logic, namely the \(\lambda \Delta \) calculus as formulated by N. J. Rehof and M. H. Sørensen [Lect. Notes Comput. Sci. 789, 516–542 (1994; Zbl 0942.03512)]. We show that there is a non-trivial extension of the hereditary substitution function of the simply-typed \(\lambda\) calculus to one for the \(\lambda \Delta \) calculus. Then hereditary substitution is used to prove normalization.
For the entire collection see [Zbl 1471.68013].
For the entire collection see [Zbl 1471.68013].
MSC:
| 03B40 | Combinatory logic and lambda calculus |
| 03B38 | Type theory |
| 03B70 | Logic in computer science |
| 03F05 | Cut-elimination and normal-form theorems |
| 68N18 | Functional programming and lambda calculus |
References:
| [1] | Andreas Abel (2006): Implementing a normalizer using sized heterogeneous types. In:In Workshop on Mathematically Structured Functional Programming, MSFP, doi:10.1017/S0956796809007266. · Zbl 1191.68152 |
| [2] | Andreas Abel & Dulma Rodriguez (2008): Syntactic Metatheory of Higher-Order Subtyping. In:Proceedings of the 22nd international workshop on Computer Science Logic, CSL ’08, Springer-Verlag, Berlin, Heidelberg, pp. 446-460, doi:10.1007/978-3-540-87531-4 32. · Zbl 1156.03311 |
| [3] | Robin Adams (2004): A Modular Hierarchy of Logical Frameworks. Ph.D. thesis. · Zbl 1100.68542 |
| [4] | R.M. Amadio & P.L. Curien (1998): Domains and lambda-calculi. Cambridge tracts in theoretical computer science, Cambridge University Press, doi:10.1017/CBO9780511983504. · Zbl 0962.03001 |
| [5] | G. Barthe, J. Hatcliff & M. Heine Sørensen (1997): A notion of classical pure type system (preliminary version).Electronic Notes in Theoretical Computer Science6, pp. 4-59, doi:10.1016/S1571-0661(05)80170-7. |
| [6] | Gilles Barthe, John Hatcliff & Morten Heine Srensen (2001): Weak normalization implies strong normalization in a class of non-dependent pure type systems.Theoretical Computer Science269(1-2), pp. 317 - 361, doi:10.1016/S0304-3975(01)00012-3. · Zbl 0983.68029 |
| [7] | Rene David & Karim Nour (2003): A short proof of the strong normalization of the simply typed lambdamucalculus.SCHEDAE INFORMATICAE12, pp. 27-33. |
| [8] | Harley Eades & Aaron Stump (2010): Hereditary Substitution for Stratified System F. In:Proof-Search in Type Theories (PSTT). |
| [9] | Jean-Yves Girard, Yves Lafont & Paul Taylor (1989): Proofs and Types (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press. · Zbl 0671.68002 |
| [10] | Harley Eades II & Aaron Stump (2011): Using the Hereditary Substitution Function in Normalization Proofs. Available athttp://metatheorem.org/wp-content/papers/qual_companion_report.pdf. |
| [11] | Felix Joachimski & Ralph Matthes (1999): Short Proofs of Normalization for the simply-typed lambdacalculus, permutative conversions and G¨odel’s T. |
| [12] | Chantal Keller & Thorsten Altenkirch (2010): Hereditary substitutions for simple types, formalized. In: Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming, MSFP ’10, ACM, New York, NY, USA, pp. 3-10, doi:10.1145/1863597.1863601. |
| [13] | D.Leivant(1991):Finitelystratifiedpolymorphism.Inf.Comput.93(1),pp.93-113, doi:10.1016/0890-5401(91)90053-5. · Zbl 0799.68041 |
| [14] | Jean-Jacques L´evy (1976): An algebraic interpretation of the K-calculus; and an application of a labelled -calculus.Theoretical Computer Science2(1), pp. 97 - 114, doi:10.1016/0304-3975(76)90009-8. · Zbl 0335.02016 |
| [15] | Michel Parigot (1992): Lambda-Mu-Calculus: An algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor:Logic Programming and Automated Reasoning,Lecture Notes in Computer Science624, Springer Berlin / Heidelberg, pp. 190-201, doi:10.1007/BFb0013061. · Zbl 0925.03092 |
| [16] | Michel Parigot (1997): Proofs of Strong Normalization for Second Order Classical Natural Deduction.Journal of Symbolic Logic62(4), pp. 1461-1479, doi:10.2307/2275652. · Zbl 0941.03063 |
| [17] | Jakob Rehof & Morten Heine Sørensen (1994): The LambdaDelta-calculus. In:Proceedings of the International Conference on Theoretical Aspects of Computer Software, TACS ’94, Springer-Verlag, London, UK, pp. 516-542, doi:10.1007/3-540-57887-0 113. · Zbl 0942.03512 |
| [18] | Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2004): A Concurrent Logical Framework: The Propositional Fragment. In Stefano Berardi, Mario Coppo & Ferruccio Damiani, editors:Types for Proofs and Programs,Lecture Notes in Computer Science3085, Springer Berlin / Heidelberg, pp. 355-377, doi:10.1007/978-3-540-24849-1 23 · Zbl 1100.68548 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
