×

Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda. (English) Zbl 1498.03044

Nalon, Cláudia (ed.) et al., Proceedings of the 15th international workshop on logical and semantic frameworks, with applications, LSFA 2020, virtual workshop, August 27–28, 2020. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 351, 187-203 (2020).
Summary: We consider a pre-existing formalization in Constructive Type Theory of the pure Lambda Calculus in its presentation in first order syntax with only one sort of names and alpha-conversion based upon multiple substitution, as well as of the system of assignment of simple types to terms. On top of it, we formalize a slick proof of strong normalization given by F. Joachimski and R. Matthes [Arch. Math. Logic 42, No. 1, 59–87 (2003; Zbl 1025.03010)] whose main lemma proceeds by complete induction on types and subordinate induction on a characterization of the strongly normalizing terms which is in turn proven sound with respect to their direct definition as the accessible part of the relation of one-step beta reduction. The proof of strong normalization itself is thereby allowed to consist just of a direct induction on the type system. The whole development has been machine-checked using the system Agda. We assess merits and drawbacks of the approach.
For the entire collection see [Zbl 1451.68025].

MSC:

03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems

Citations:

Zbl 1025.03010
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abel, A.; Allais, G.; Hameer, A.; Pientka, B.; Momigliano, A.; Schäfer, S.; Stark, K., POPLMark reloaded: Mechanizing proofs by logical relations, Journal of Functional Programming, 29 (2019) · Zbl 1442.68257
[2] Copello, E., Agda library for Formal metatheory of the lambda calculus using Stoughton’s substitution, Available at · Zbl 1383.03021
[3] Copello, E.; Szasz, N.; Tasistro, Álvaro, Formal metatheory of the lambda calculus using Stoughton’s substitution, Theoretical Computer Science, 685, 65-82 (2017) · Zbl 1383.03021
[4] Copello, E.; Szasz, N.; Tasistro, Álvaro, Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory, The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017). The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017), Electronic Notes in Theoretical Computer Science, 338, 79-95 (2018) · Zbl 1433.68542
[5] Copello, E.; Tasistro, Álvaro; Szasz, N.; Bove, A.; Fernández, M., Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory, Electronic Notes in Theoretical Computer Science, 323, 109-124 (2016) · Zbl 1395.68085
[6] Copes, M.; Szasz, N.; Tasistro, A., Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution, (Blanqui, F.; Reis, G., Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Oxford, UK, 7th July 2018. Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Oxford, UK, 7th July 2018, Electronic Proceedings in Theoretical Computer Science, vol. 274 (2018)), 27-41
[7] Curry, H. B.; Feys, R., Combinatory Logic, Volume I (1958), North-Holland, xvi+417 pp.; second printing 1968 · Zbl 0175.27601
[8] Joachimski, F.; Matthes, R., Short Proofs of Normalization for the simply-typed λ-calculus, permutative conversions and Gödel’s T, Archive for Mathematical Logic, 42, 59-87 (2003) · Zbl 1025.03010
[9] Nipkow, T.; Berghofer, S., Fundamental Properties of Lambda-calculus (2019), available from
[10] Norell, U., Towards a Practical Programming Language Based on Dependent Type Theory (2007), Department of Computer Science and Engineering, Chalmers University of Technology, Ph.D. thesis
[11] Stoughton, A., Substitution revisited, Theoretical Computer Science, 59, 317-325 (1988) · Zbl 0651.03008
[12] Urban, C.; Tasson, C., Nominal Techniques in Isabelle/HOL, (Nieuwenhuis, R., Automated Deduction - CADE-20. Automated Deduction - CADE-20, Lecture Notes in Computer Science, vol. 3632 (2005), Springer: Springer Berlin Heidelberg), 38-53 · Zbl 1135.68561
[13] van Raamsdonk, F.; Severi, P., On Normalisation (1995), Centrum voor Wiskunde en Informatica (CWI): Centrum voor Wiskunde en Informatica (CWI) Amsterdam, Technical report
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.