The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)

DOI10.1016/S1571-0661(04)00277-4zbMath1268.68057MaRDI QIDQ2841232

René Vestergaard, James Brotherston

Publication date: 24 July 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (3)

Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations ⋮ A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. ⋮ Alpha equivalence equalities

Uses Software

• Isabelle
• Isabelle/HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Substitution revisited
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• More Church-Rosser proofs (in Isabelle/HOL)
• Some lambda calculus and type theory formalized
• A mechanical proof of the Church-Rosser theorem
• Residual theory in λ-calculus: a formal development
• Proving Properties of Programs by Structural Induction
• Parallel reductions in \(\lambda\)-calculus

This page was built for publication: The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)