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
Kanovich, Max A note on rewriting proofs and Fibonacci numbers. (English) Zbl 1133.05006 Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 284-292 (2007). MSC: 05A17 05A20 68Q42 68T15 PDFBibTeX XMLCite \textit{M. Kanovich}, Lect. Notes Comput. Sci. 4514, 284--292 (2007; Zbl 1133.05006) 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
Vejjajiva, Pimpen; Hall, Mark E. A lambda-calculus with patterns. (English) Zbl 1070.03506 Proceedings of the international conference on algebra and its applications (ICAA 2002), Chulalongkorn University, Bangkok, Thailand, March 18–20, 2002. Bangkog: Chulalongkorn University, Department of Mathematics (ISBN 970-13-2182-1). 266-277 (2002). MSC: 03B40 PDFBibTeX XMLCite \textit{P. Vejjajiva} and \textit{M. E. Hall}, in: Proceedings of the international conference on algebra and its applications (ICAA 2002), Chulalongkorn University, Bangkok, Thailand, March 18--20, 2002. Bangkog: Chulalongkorn University, Department of Mathematics. 266--277 (2002; Zbl 1070.03506)
Struth, Georg Calculating Church-Rosser proofs in Kleene algebra. (English) Zbl 1027.68071 de Swart, Harrie C. M. (ed.), Relational methods in computer science. 6th international conference, RelMiCS 2001 and 1st workshop of COST Action 274 TARSKI, Oisterwijk, The Netherlands, October 16-21, 2001. Revised papers. Berlin: Springer. Lect. Notes Comput. Sci. 2561, 276-290 (2002). MSC: 68Q42 68Q70 03B40 PDFBibTeX XMLCite \textit{G. Struth}, Lect. Notes Comput. Sci. 2561, 276--290 (2002; Zbl 1027.68071) Full Text: Link
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
Aczel, Peter Notes on the simply typed lambda calculus. (English) Zbl 0933.03007 Berger, Ulrich (ed.) et al., Computational logic. Proceedings of the NATO ASI, Marktoberdorf, Germany, July 29–August 10, 1997. Berlin: Springer. NATO ASI Ser., Ser. F, Comput. Syst. Sci. 165, 57-97 (1999). MSC: 03B40 03-02 03B20 03F03 03F35 03F50 PDFBibTeX XMLCite \textit{P. Aczel}, NATO ASI Ser., Ser. F, Comput. Syst. Sci. 165, 57--97 (1999; Zbl 0933.03007)
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
Ginisti, Jean-Pierre Combinatory logic. (La logique combinatoire.) (French) Zbl 0873.03011 Que sais-je? Paris: Presses Universitaires de France. 127 p. (1997). Reviewer: A.Cantini (Firenze) MSC: 03B40 03-01 00A06 PDFBibTeX XMLCite \textit{J.-P. Ginisti}, La logique combinatoire. Paris: Presses Universitaires de France (1997; Zbl 0873.03011)
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
de Groote, Philippe Defining \(\lambda\)-typed \(\lambda\)-calculi by axiomatizing the typing relation. (English) Zbl 0797.68144 Enjalbert, Patrice (ed.) et al., STACS 93. 10th annual symposium on theoretical aspects of computer science, Würzburg, Germany, February 25-27, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 665, 712-723 (1993). MSC: 68T15 03B40 68Q45 PDFBibTeX XMLCite \textit{P. de Groote}, Lect. Notes Comput. Sci. 665, 712--723 (1993; Zbl 0797.68144)
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
Ehrig, Hartmut; Parisi-Presicce, Francesco Algebraic specification grammars: A junction between module specifications and graph grammars. (English) Zbl 0765.68087 Graph grammars and their application to computer science, Proc. 4th Int. Workshop, Bremen/Ger. 1990, Lect. Notes Comput. Sci. 532, 292-310 (1991). MSC: 68Q42 68Q60 PDFBibTeX XMLCite \textit{H. Ehrig} and \textit{F. Parisi-Presicce}, Lect. Notes Comput. Sci. 532, 292--310 (1991; Zbl 0765.68087)
Ehrig, Hartmut; Habel, Annegret; Parisi-Presicce, Francesco From graph grammars to high level replacement systems. (English) Zbl 0765.68088 Graph grammars and their application to computer science, Proc. 4th Int. Workshop, Bremen/Ger. 1990, Lect. Notes Comput. Sci. 532, 269-291 (1991). MSC: 68Q42 68Q60 PDFBibTeX XMLCite \textit{H. Ehrig} et al., Lect. Notes Comput. Sci. 532, 269--291 (1991; Zbl 0765.68088)
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
Okada, Mitsuhiro A logical analysis on theory of conditional rewriting. (English) Zbl 0667.68106 Conditional term rewriting systems, 1st. int. Workshop, Orsay/France 1987, Lect. Notes Comput.Sci. 308, 179-196 (1988). Reviewer: T.Tammet MSC: 68T15 03B35 PDFBibTeX XML
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
Benninghofen, B.; Kemmerich, S.; Richter, M. M. [Otto, F.] Systems of reductions. (English) Zbl 0636.68027 Lecture Notes in Computer Science, 277. Berlin etc.: Springer-Verlag. X, 265 p.; DM 40.50 (1987). Reviewer: J.Zlatuska MSC: 68Q65 08A50 20F10 20M35 03D60 68Q25 68Q45 68T15 68-02 03B25 PDFBibTeX XML
Padawitz, Peter Strategy-controlled reduction and narrowing. (English) Zbl 0635.68105 Rewriting techniques and applications, Proc. 2nd Int. Conf., Bordeaux/France 1987, Lect. Notes Comput. Sci. 256, 242-252 (1987). MSC: 68T15 03B35 PDFBibTeX XML
Toyama, Yoshihito How to prove equivalence of term rewriting systems without induction. (English) Zbl 0642.68033 Automated deduction, Proc. 8th Int. Conf., Oxford/Engl. 1986, Lect. Notes Comput. Sci. 230, 118-127 (1986). MSC: 68Q65 68T15 08B05 PDFBibTeX XML
Winkler, F.; Buchberger, B. A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. (English) Zbl 0607.03003 Algebra, combinatorics and logic in computer science, Colloq. Györ/Hung. 1983, Vol. 2, Colloq. Math. Soc. János Bolyai 42, 849-869 (1986). MSC: 03B35 68T15 08B05 PDFBibTeX XML
Perdrix, H. Propriétés Church-Rosser de systèmes de réecriture equationnels ayant la propriété de termination faible. (French) Zbl 0583.68005 Theoretical aspects of computer science, Symp., Paris 1984, Lect. Notes Comput. Sci. 166, 97-108 (1984). Reviewer: A.Pettorossi MSC: 68Q65 68T15 68Q55 PDFBibTeX XML
Winkler, Franz The Church Rosser property in computer algebra and special theorem proving: an investigation of critical pair/completion algorithms. (English) Zbl 0562.68023 Dissertationen der Johannes Kepler-Universität Linz, 49. Linz: Johannes Kepler-Universität; Wien: Verband der Wissenschaftlichen Gesellschaften Österreichs (VWGÖ) 193 p. ÖS 180.00; DM 27.00 (1984). Reviewer: V.Calmatuianu MSC: 68W30 68T15 68-02 PDFBibTeX XML
Rice, Monique The construction of a complete minimal set of contextual normal forms. (English) Zbl 0549.68022 Computer algebra, EUROCAL ’83, Proc. Conf., London 1983, Lect. Notes Comput. Sci. 162, 255-266 (1983). MSC: 68Q65 PDFBibTeX XML
Jouannaud, Jean-Pierre Confluent and coherent equational term rewriting systems application to proofs in abstract data types. (English) Zbl 0522.68013 Trees in algebra and programming, CAAP ’83, Proc. 8th Colloq., L’Aquila/Italy 1983, Lect. Notes Comput. Sci. 159, 269-283 (1983). MSC: 68Q60 68W30 68P05 68T15 08A50 03F05 PDFBibTeX XML
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
Curry, Haskell B. Some philosophical aspects of combinatory logic. (English) Zbl 0479.03005 The Kleene Symp., Proc., Madison/Wis. 1978, Stud. Logic Found. Math., Vol. 101, 85-101 (1980). MSC: 03B40 03A05 03-02 03-03 PDFBibTeX XML
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
van Daalen, Diederik Ton The language theory of Automath. (English) Zbl 0422.68045 Eindhoven: Technische Hogeschool. VI, 309 p. (1980). MSC: 68T15 68T99 68-02 03B40 03B35 03-02 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)