Paper Info
Title
Strong Normalization for the Simply-Typed Lambda Calculus in Constructive Type Theory Using Agda.
Abstract
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 Joachimski and Matthes 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.
Year
DOI
Venue
2020
10.1016/j.entcs.2020.08.010
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
Keywords
DocType
Volume
Formal Metatheory,Lambda Calculus,Constructive Type Theory
Conference
351
ISSN
Citations 
PageRank 
1571-0661
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Sebastián Urciuoli100.34
Álvaro Tasistro2212.99
Nora Szasz3528.48