Shankar, N. A mechanical proof of the Church-Rosser theorem. (English) Zbl 0654.68103 J. Assoc. Comput. Mach. 35, No. 3, 475-522 (1988). Reviewer: A.Leitsch MSC: 68T15 03B35 03B40 PDFBibTeX XMLCite \textit{N. Shankar}, J. Assoc. Comput. Mach. 35, No. 3, 475--522 (1988; Zbl 0654.68103) Full Text: DOI
Huet, Gerard Confluent reductions: Abstract properties and applications to term rewriting systems. (English) Zbl 0458.68007 J. Assoc. Comput. Mach. 27, 797-821 (1980). MSC: 68Q65 68Q60 PDFBibTeX XMLCite \textit{G. Huet}, J. Assoc. Comput. Mach. 27, 797--821 (1980; Zbl 0458.68007) Full Text: DOI