scientific article; zbMATH DE number 1953901

MaRDI QIDQ4415087zbMATH OpenFDO

Authors Georg Struth

Publication date 28 July 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2561/25610276.htm

zbMATH Keywords

\(\lambda\)-calculusChurch-Rosser theoremformal mathematicsKleene algebrarewriting

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42) Algebraic theory of languages and automata (68Q70)

Recommendations

• Abstract abstract reduction
• Church–Rosser Made Easy
• More Church-Rosser proofs (in Isabelle/HOL)
• More Church-Rosser proofs (in Isabelle/HOL)
• A mechanical proof of the Church-Rosser theorem

Cited in

(7)

• The Church Rosser theorem for strong reduction in combinatory logic
• Abstract strategies and coherence
• Automated Reasoning for Hybrid Systems — Two Case Studies —
• More Church-Rosser proofs (in Isabelle/HOL)
• Algebraic coherent confluence and higher globular Kleene algebras
• Diagonalisation and Church's Thesis: Kleene's Homework
• Abstract abstract reduction

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4415087)