Kosterec, Miloš Substitution contradiction, its resolution and the Church-Rosser theorem in TIL. (English) Zbl 1484.03006 J. Philos. Log. 49, No. 1, 121-133 (2020). MSC: 03A05 03B40 03B60 PDFBibTeX XMLCite \textit{M. Kosterec}, J. Philos. Log. 49, No. 1, 121--133 (2020; Zbl 1484.03006) Full Text: DOI
Fujita, Ken-etsu The Church-Rosser theorem and quantitative analysis of witnesses. (English) Zbl 1436.03104 Inf. Comput. 263, 52-56 (2018). MSC: 03B40 PDFBibTeX XMLCite \textit{K.-e. Fujita}, Inf. Comput. 263, 52--56 (2018; Zbl 1436.03104) Full Text: DOI
Adams, Robin Pure type systems with judgemental equality. (English) Zbl 1088.68030 J. Funct. Program. 16, No. 2, 219-246 (2006). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{R. Adams}, J. Funct. Program. 16, No. 2, 219--246 (2006; Zbl 1088.68030) Full Text: DOI