Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
From MaRDI portal
Publication:5022932
DOI10.1017/S0960129521000335OpenAlexW3217631441MaRDI QIDQ5022932
Nora Szasz, Álvaro Tasistro, Ernesto Copello
Publication date: 20 January 2022
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129521000335
Combinatory logic and lambda calculus (03B40) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Program extraction from normalization proofs
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- Nominal logic, a first order theory of names and binding
- The locally nameless representation
- Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
- Formal metatheory of the lambda calculus using Stoughton's substitution
- Alpha-structural recursion and induction
- Barendregt’s Variable Convention in Rule Inductions
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
- POPLMark reloaded: Mechanizing proofs by logical relations
- Automated Deduction – CADE-20
- Parallel reductions in \(\lambda\)-calculus
This page was built for publication: Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
