Alpha-structural induction and recursion for the lambda calculus in constructive type theory

DOI10.1016/j.entcs.2016.06.008zbMath1395.68085OpenAlexW2461095491WikidataQ113317681 ScholiaQ113317681MaRDI QIDQ1744410

Ernesto Copello, Maribel Fernández, Nora Szasz, Álvaro Tasistro, Ana Bove

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2016.06.008

zbMATH Keywords

constructive type theorylambda calculusformal metatheory

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items

Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ Nominal Sets in Agda - A Fresh and Immature Mechanization ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Uses Software

• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
• A new approach to abstract syntax with variable binding
• Viewing \({\lambda}\)-terms through maps
• Substitution revisited
• Nominal logic, a first order theory of names and binding
• The locally nameless representation
• Engineering formal metatheory
• Alpha-structural recursion and induction
• Automated Deduction – CADE-20
• Theorem Proving in Higher Order Logics