Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
From MaRDI portal
Publication:853738
DOI10.1007/S10990-006-8745-7zbMath1105.68093OpenAlexW1981019433MaRDI QIDQ853738
Publication date: 17 November 2006
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10990-006-8745-7
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items (7)
A formalized general theory of syntax with bindings ⋮ Nominal techniques in Isabelle/HOL ⋮ A formalized general theory of syntax with bindings: extended version ⋮ On the Role of Names in Reasoning about λ-tree Syntax Specifications ⋮ Mechanised Computability Theory ⋮ Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem ⋮ Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The lambda calculus. Its syntax and semantics. Rev. ed.
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- Nominal logic, a first order theory of names and binding
- Some lambda calculus and type theory formalized
- Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
- The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)
- Residual theory in λ-calculus: a formal development
- Defining functions on equivalence classes
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
This page was built for publication: Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
