A simplified proof of the Church-Rosser theorem

DOI10.1007/S11225-013-9470-YMaRDI QIDQ2016071zbMATH OpenOpenAlexFDO

Authors Yuichi Komori, Naosuke Matsuda, Fumika Yamakawa

Publication date 19 June 2014

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11225-013-9470-y

zbMATH Keywords

\(\lambda\)-calculusconfluence theoremparallel reductionChurch-Rosser theoremTakahashi translation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Church–Rosser Made Easy
• More Church-Rosser proofs (in Isabelle/HOL)
• Parallel reductions in \(\lambda\)-calculus
• Complexity Versus the Church‐Rosser Property and Confluence
• More Church-Rosser proofs (in Isabelle/HOL)

Cites work

• scientific article; zbMATH DE number 5318491 (Why is no real title available?)
• Parallel reductions in \(\lambda\)-calculus
• Parallel reductions in \(\lambda\)-calculus
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(7)

• A formal system of reduction paths for parallel reduction
• Strong reduction of combinatory calculus with streams
• Church–Rosser Made Easy
• Z property for the shuffling calculus
• Reduction rules for intuitionistic \(\lambda\rho\)-calculus
• Compositional Z: confluence proofs for permutative conversion
• Is sized typing for Coq practical?

This page was built for publication: A simplified proof of the Church-Rosser theorem

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