{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T02:25:50Z","timestamp":1778293550469,"version":"3.51.4"},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540565175","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037114","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"306-317","source":"Crossref","is-referenced-by-count":27,"title":["Orthogonal higher-order rewrite systems are confluent"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"P. Aczel. A general Church-Rosser theorem. Technical report, University of Manchester, 1978."},{"key":"21_CR2","unstructured":"H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, 2nd edition, 1984."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symp. Logic in Computer Science, pages 82\u201390, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Formal Models and Semantics, Handbook of Theoretical Computer Science, Vol. B, pages 243\u2013320. Elsevier \u2014 The MIT Press, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"D. J. Dougherty. Adding algebraic rewriting to the untyped lambda-calculus. In R. V. Book, editor, Proc. 4th Int. Conf. Rewriting Techniques and Applications, pages 37\u201348. LNCS 488, 1991.","DOI":"10.1007\/3-540-53904-2_84"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"A. Felty. A logic-programming approach to implementing higher-order term rewriting. In L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, editors, Extensions of Logic Programming, Proc. 2nd Int. Workshop, pages 135\u2013158. LNCS 596, 1992.","DOI":"10.1007\/BFb0013606"},{"key":"21_CR7","unstructured":"J. Gallier. Constructive Logics. Part I. Technical Report 8, DEC Paris Research Laboratory, 1991."},{"key":"21_CR8","unstructured":"J. Hindley and J. P. Seldin. Introduction to Combinators and \u03bb-Calculus. Cambridge University Press, 1986."},{"key":"21_CR9","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet. Confluent reductions: Abstract properties and applications to term rewritingsystems. J. ACM, 27:797\u2013821, 1980.","journal-title":"J. ACM"},{"key":"21_CR10","volume-title":"Mathematical Centre Tracts 127","author":"J. W. Klop","year":"1980","unstructured":"J. W. Klop. Combinatory Reduction Systems. Mathematical Centre Tracts 127. Mathematisch Centrum, Amsterdam, 1980."},{"key":"21_CR11","volume-title":"Technical Report CS-R9073","author":"J. W. Klop","year":"1990","unstructured":"J. W. Klop. Term rewriting systems. Technical Report CS-R9073, CWI, Amsterdam, 1990."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In P. Schroeder-Heister, editor, Extensions of Logic Programming, pages 253\u2013281. LNCS 475, 1991.","DOI":"10.1007\/BFb0038698"},{"key":"21_CR13","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/0020-0190(92)90155-O","volume":"41","author":"F. M\u00fcller","year":"1992","unstructured":"F. M\u00fcller. Confluence of the lambdacalculus with left-linear algebraic rewriting. Information Processing Letters, 41:293\u2013299, 1992.","journal-title":"Information Processing Letters"},{"key":"21_CR14","unstructured":"G. Nadathur and D. Miller. An overview of \u03bbProlog. In R. A. Kowalski and K. A. Bowen, editors, Proc. 5th Int. Logic Programming Conference, pages 810\u2013827. MIT Press, 1988."},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, pages 342\u2013349, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"21_CR16","volume-title":"Technical report","author":"T. Nipkow","year":"1992","unstructured":"T. Nipkow. Functional unification of higher-order patterns. Technical report, TU M\u00fcnchen, Institut f\u00fcr Informatik, 1992."},{"key":"21_CR17","unstructured":"L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013385. Academic Press, 1990."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"S. Stenlund. Combinators, \u03bb-Terms, and Proof Theory. D. Reidel, 1972.","DOI":"10.1007\/978-94-010-2913-1"},{"key":"21_CR19","volume-title":"Technical Report CS-R9234","author":"F. Raamsdonk van","year":"1992","unstructured":"F. van Raamsdonk. A simple proof of confluence for weakly orthogonal combinatory reduction systems. Technical Report CS-R9234, CWI, Amsterdam, 1992."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037114.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:22:06Z","timestamp":1607552526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0037114","relation":{},"subject":[]}}