A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.

DOI10.1016/S0890-5401(03)00023-3zbMath1054.68028MaRDI QIDQ1401936

James Brotherston, René Vestergaard

Publication date: 19 August 2003

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

Theorem proving\({\lambda}\)-CalculusBarendregt's Variable ConventionConfluenceStructural induction and recursion

Mathematics Subject Classification ID

Related Items (8)

Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations ⋮ Ground confluence and strong commutation modulo alpha-equivalence in nominal rewriting ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus ⋮ Completeness and Herbrand theorems for nominal logic ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Uses Software

• Isabelle/HOL
• Twelf

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Substitution revisited
• An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus
• More Church-Rosser proofs (in Isabelle/HOL)
• Some lambda calculus and type theory formalized
• The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)
• A mechanical proof of the Church-Rosser theorem
• Completion of a Set of Rules Modulo a Set of Equations
• Residual theory in λ-calculus: a formal development
• Proving Properties of Programs by Structural Induction
• Some Properties of Conversion
• Parallel reductions in \(\lambda\)-calculus
• Primitive recursion for higher-order abstract syntax

This page was built for publication: A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.