A simplified proof of the Church-Rosser theorem

DOI10.1007/S11225-013-9470-YzbMATH Open1338.03017OpenAlexW2054680866MaRDI QIDQ2016071FDOQ2016071

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

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)

zbMATH Keywords

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Parallel reductions in \(\lambda\)-calculus
• Parallel reductions in \(\lambda\)-calculus

Cited In (7)

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

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)