More Church-Rosser proofs (in Isabelle/HOL)

DOI10.1007/3-540-61511-3_125zbMath1412.68248OpenAlexW2098856123MaRDI QIDQ4647561

Tobias Nipkow

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_125

zbMATH Keywords

typed lambda-calculusexplicit substitutionsubstitution lemmalambda-termstandard proof

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Proof Pearl: Abella Formalization of λ-Calculus Cube Property

Uses Software

• Isabelle
• ML
• Isabelle/HOL
• HOL
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Isabelle. A generic theorem prover
• Metamathematics, Machines and Gödel's Proof
• Residual theory in λ-calculus: a formal development
• Parallel reductions in \(\lambda\)-calculus