More Church-Rosser proofs (in Isabelle/HOL)
From MaRDI portal
Publication:1595924
DOI10.1023/A:1006496715975zbMath0958.03011OpenAlexW1527418902MaRDI QIDQ1595924
Publication date: 18 February 2001
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1006496715975
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle ⋮ Unnamed Item ⋮ A formalization of the Knuth-Bendix(-Huet) critical pair theorem ⋮ A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ A solution to the PoplMark challenge based on de Bruijn indices ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ A PVS Theory for Term Rewriting Systems ⋮ A Mechanized Model of the Theory of Objects ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Equational Reasoning with Applicative Functors ⋮ The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Abstract abstract reduction
Uses Software
