Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

DOI10.1017/S0960129521000335MaRDI QIDQ5022932zbMATH OpenOpenAlexFDO

Authors Ernesto Copello, Nora Szasz, Álvaro Tasistro

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

zbMATH Keywords

constructive type theoryformalized metatheorylambda calculusnominal syntaxproof assistants

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• 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 induction and recursion for the lambda calculus in constructive type theory
• Some lambda calculus and type theory formalized
• Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda

Cites work

• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• A head-to-head comparison of de Bruijn indices and names
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Alpha-structural recursion and induction
• Automated Deduction – CADE-20
• Barendregt’s Variable Convention in Rule Inductions
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
• Nominal logic, a first order theory of names and binding
• Nominal reasoning techniques in Coq (extended abstract)
• Parallel reductions in \(\lambda\)-calculus
• POPLMark reloaded: mechanizing proofs by logical relations
• Program extraction from normalization proofs
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The locally nameless representation

Cited in

(5)

• Formal metatheory of the lambda calculus using Stoughton's substitution
• scientific article; zbMATH DE number 1722714 (Why is no real title available?)
• Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
• More Church-Rosser proofs in \textsc{Beluga}
• Modular abstract syntax trees (MAST): substitution tensors with second-class sorts

Describes a project that uses

Uses Software

• PoplMark
• Nominal Isabelle

This page was built for publication: Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5022932)