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

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

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.