Name
Title | ||
|---|---|---|
Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention |
Abstract | ||
|---|---|---|
Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with alpha-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church-Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1017/S0960129521000335 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
Formalized metatheory, nominal syntax, Lambda Calculus, constructive type theory, proof assistants | Journal | 31 |
Issue | ISSN | Citations |
3 | 0960-1295 | 0 |
PageRank | References | Authors |
0.34 | 0 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ernesto Copello | 1 | 3 | 2.05 |
| Nora Szasz | 2 | 52 | 8.48 |
| Álvaro Tasistro | 3 | 21 | 2.99 |