Alpha-structural induction and recursion for the lambda calculus in constructive type theory
From MaRDI portal
Publication:1744410
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
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
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