A simplified proof of the Church-Rosser theorem

DOI10.1007/S11225-013-9470-YzbMath1338.03017OpenAlexW2054680866MaRDI QIDQ2016071

Fumika Yamakawa, Naosuke Matsuda, Yuichi Komori

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\)-calculusparallel reductionconfluence theoremChurch-Rosser theoremTakahashi translation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (6)

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

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Parallel reductions in \(\lambda\)-calculus
• Parallel reductions in \(\lambda\)-calculus

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