Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations

DOI10.1007/s10990-006-8745-7zbMath1105.68093OpenAlexW1981019433MaRDI QIDQ853738

Michael Norrish

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

zbMATH Keywords

Barendregt variable convention

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

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

• Nominal Isabelle

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