Fujita, Ken-etsu A formal system of reduction paths for parallel reduction. (English) Zbl 1433.68190 Theor. Comput. Sci. 813, 327-340 (2020). MSC: 68Q42 03B40 68R10 PDFBibTeX XMLCite \textit{K.-e. Fujita}, Theor. Comput. Sci. 813, 327--340 (2020; Zbl 1433.68190) Full Text: DOI
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
Komori, Yuichi; Matsuda, Naosuke; Yamakawa, Fumika A simplified proof of the Church-Rosser theorem. (English) Zbl 1338.03017 Stud. Log. 102, No. 1, 175-183 (2014). MSC: 03B40 PDFBibTeX XMLCite \textit{Y. Komori} et al., Stud. Log. 102, No. 1, 175--183 (2014; Zbl 1338.03017) Full Text: DOI
Kozen, Dexter Church-Rosser made easy. (English) Zbl 1231.03012 Fundam. Inform. 103, No. 1-4, 129-136 (2010). MSC: 03B40 PDFBibTeX XMLCite \textit{D. Kozen}, Fundam. Inform. 103, No. 1--4, 129--136 (2010; Zbl 1231.03012) Full Text: DOI
Mirasyedioğlu, Şeref; Güyer, Tolga A symbolic and algebraic computation based lambda-Boolean reduction machine via PROLOG. (English) Zbl 1095.68751 Appl. Math. Comput. 176, No. 1, 65-75 (2006). MSC: 68W30 03B40 68N17 68Q05 68Q42 PDFBibTeX XMLCite \textit{Ş. Mirasyedioğlu} and \textit{T. Güyer}, Appl. Math. Comput. 176, No. 1, 65--75 (2006; Zbl 1095.68751) Full Text: DOI Link
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
Nipkow, Tobias More Church-Rosser proofs (in Isabelle/HOL). (English) Zbl 0958.03011 J. Autom. Reasoning 26, No. 1, 51-66 (2001). MSC: 03B35 03B40 68T15 PDFBibTeX XMLCite \textit{T. Nipkow}, J. Autom. Reasoning 26, No. 1, 51--66 (2001; Zbl 0958.03011) Full Text: DOI
Burr, Wolfgang; Hartung, Volker A characterization of the \(\Sigma_1\)-definable functions of \(\text{KP}\omega+(\text{uniform AC})\). (English) Zbl 0913.03051 Arch. Math. Logic 37, No. 3, 199-214 (1998). Reviewer: Benjamin Blankertz (Münster) MSC: 03F10 03F25 03E70 03E25 PDFBibTeX XMLCite \textit{W. Burr} and \textit{V. Hartung}, Arch. Math. Logic 37, No. 3, 199--214 (1998; Zbl 0913.03051) Full Text: DOI
Banach, R. MONSTR V – transitive coercing semantics and the Church-Rosser property. (English) Zbl 0960.68083 J. UCS 3, No. 12, 1283-1336 (1997). MSC: 68Q42 68Q55 PDFBibTeX XMLCite \textit{R. Banach}, J. UCS 3, No. 12, 1283--1336 (1997; Zbl 0960.68083) Full Text: Link
Laneve, Cosimo; Montanari, Ugo Axiomatizing permutation equivalence. (English) Zbl 0884.68070 Math. Struct. Comput. Sci. 6, No. 3, 219-249 (1996). Reviewer: N.Bernard (Le Bourget du Lac) MSC: 68Q42 03B40 68Q55 PDFBibTeX XMLCite \textit{C. Laneve} and \textit{U. Montanari}, Math. Struct. Comput. Sci. 6, No. 3, 219--249 (1996; Zbl 0884.68070) Full Text: DOI
David, René A simple proof of basic results in \(\lambda\) calculus. (Une preuve simple de résultats classiques en \(\lambda\) calcul.) (French. Abridged English version) Zbl 0830.03003 C. R. Acad. Sci., Paris, Sér. I 320, No. 11, 1401-1406 (1995). MSC: 03B40 PDFBibTeX XMLCite \textit{R. David}, C. R. Acad. Sci., Paris, Sér. I 320, No. 11, 1401--1406 (1995; Zbl 0830.03003)
Takahashi, Masako Parallel reductions in \(\lambda\)-calculus. (English) Zbl 0827.68060 Inf. Comput. 118, No. 1, 120-127 (1995). MSC: 68W30 PDFBibTeX XMLCite \textit{M. Takahashi}, Inf. Comput. 118, No. 1, 120--127 (1995; Zbl 0827.68060) Full Text: DOI
López-Escobar, E. G. K. Graphical representation of the theorem of Church and Rosser. (Spanish) Zbl 0801.03014 Rev. Colomb. Mat. 27, No. 3-4, 267-280 (1993). MSC: 03B40 PDFBibTeX XMLCite \textit{E. G. K. López-Escobar}, Rev. Colomb. Mat. 27, No. 3--4, 267--280 (1993; Zbl 0801.03014) Full Text: EuDML
Fülöp, Zoltán; Vágvölgyi, Sándor Ground term rewriting rules for the word problem of ground term equations. (English) Zbl 0757.68069 Bull. EATCS 45, 186-201 (1991). MSC: 68Q42 68Q05 68T15 PDFBibTeX XMLCite \textit{Z. Fülöp} and \textit{S. Vágvölgyi}, Bull. EATCS 45, 186--201 (1991; Zbl 0757.68069)
Postma, Stef W. The \(\Sigma{}\lambda\)-calculus and derived program forms. (English) Zbl 0741.03005 Quaest. Math. 14, No. 2, 137-159 (1991). MSC: 03B40 68Q10 03B70 68N01 03B50 PDFBibTeX XMLCite \textit{S. W. Postma}, Quaest. Math. 14, No. 2, 137--159 (1991; Zbl 0741.03005) Full Text: DOI
Kawahara, Yasuo Pushout-complements and basic concepts of grammars in toposes. (English) Zbl 0723.18004 Theor. Comput. Sci. 77, No. 3, 267-289 (1990). Reviewer: Y.Diers (Faches-Thumesnil) MSC: 18B25 68Q42 18A30 18A10 PDFBibTeX XMLCite \textit{Y. Kawahara}, Theor. Comput. Sci. 77, No. 3, 267--289 (1990; Zbl 0723.18004) Full Text: DOI
López-Escobar, E. G. K. Remarks on the Church-Rosser property. (English) Zbl 0715.03025 J. Symb. Log. 55, No. 1, 106-112 (1990). Reviewer: A.A.Mullin MSC: 03F50 03B40 03F05 PDFBibTeX XMLCite \textit{E. G. K. López-Escobar}, J. Symb. Log. 55, No. 1, 106--112 (1990; Zbl 0715.03025) Full Text: DOI
Narendran, Paliath; Otto, Friedrich Some polynomial-time algorithms for finite monadic Church-Rosser Thue systems. (English) Zbl 0677.68050 Theor. Comput. Sci. 68, No. 3, 319-332 (1989). MSC: 68Q25 68Q65 03D03 03B25 68T15 68T99 PDFBibTeX XMLCite \textit{P. Narendran} and \textit{F. Otto}, Theor. Comput. Sci. 68, No. 3, 319--332 (1989; Zbl 0677.68050) Full Text: DOI
Yokouchi, Hirofumi Church-Rosser theorem for a rewriting system on categorical combinators. (English) Zbl 0672.03006 Theor. Comput. Sci. 65, No. 3, 271-290 (1989). Reviewer: A.Pettorossi MSC: 03B40 68N01 PDFBibTeX XMLCite \textit{H. Yokouchi}, Theor. Comput. Sci. 65, No. 3, 271--290 (1989; Zbl 0672.03006) Full Text: DOI
Desclés, Jean-Pierre Théorème de Church-Rosser et structuration des langues naturelles. (Church-Rosser theorem and structuration of natural languages). (French) Zbl 0663.03006 Math. Inf. Sci. Hum. 103, 67-92 (1988). MSC: 03B40 03B65 PDFBibTeX XMLCite \textit{J.-P. Desclés}, Math. Inf. Sci. Hum. 103, 67--92 (1988; Zbl 0663.03006) Full Text: Numdam EuDML
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
Kapur, Deepak; Musser, David R.; Narendran, Paliath Only prime superpositions need be considered in the Knuth-Bendix completion procedure. (English) Zbl 0651.68029 J. Symb. Comput. 6, No. 1, 19-36 (1988). MSC: 68Q65 68W30 68T15 PDFBibTeX XMLCite \textit{D. Kapur} et al., J. Symb. Comput. 6, No. 1, 19--36 (1988; Zbl 0651.68029) Full Text: DOI
Mirasyedioğlu, Şeref \(\lambda\)-Boolean theory. (English) Zbl 0656.03008 Int. Logic Rev. 35, 13-27 (1987). Reviewer: P.Materna MSC: 03B40 PDFBibTeX XMLCite \textit{Ş. Mirasyedioğlu}, Int. Logic Rev. 35, 13--27 (1987; Zbl 0656.03008)
Oyamaguchi, Michio The Church-Rosser property for ground term-rewriting systems is decidable. (English) Zbl 0641.68044 Theor. Comput. Sci. 49, 43-79 (1987). Reviewer: J.Zlatuska MSC: 68Q65 20M05 68Q45 68T15 08A50 20M35 PDFBibTeX XMLCite \textit{M. Oyamaguchi}, Theor. Comput. Sci. 49, 43--79 (1987; Zbl 0641.68044) Full Text: DOI
Pottinger, Garrel The Church-Rosser theorem for the typed lambda-calculus with pairing pairing. (English) Zbl 0476.03026 Notre Dame J. Formal Logic 22, 264-268 (1981). MSC: 03B40 PDFBibTeX XMLCite \textit{G. Pottinger}, Notre Dame J. Formal Logic 22, 264--268 (1981; Zbl 0476.03026) 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
Pottinger, Garrel The Church-Rosser theorem for the typed \(\lambda\)-calculus with surjective pairing. (English) Zbl 0423.03009 Notre Dame J. Formal Logic (to appear). MSC: 03B40 PDFBibTeX XML
Ehrig, H.; Kreowski, H.-J. Algebraic theory of graph grammars applied to consistency and synchronization in data base systems. (English) Zbl 0395.68074 Appl. Comput. Sci., Ber. Prakt. Inf. 13, 227-243 (1979). MSC: 68Q45 68P05 PDFBibTeX XMLCite \textit{H. Ehrig} and \textit{H. J. Kreowski}, Appl. Comput. Sci., Ber. Prakt. Inf. 13, 227--243 (1979; Zbl 0395.68074)