{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T22:56:07Z","timestamp":1765666567720},"reference-count":41,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1998,2,1]],"date-time":"1998-02-01T00:00:00Z","timestamp":886291200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":5645,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1998,2]]},"DOI":"10.1016\/s0304-3975(97)00143-6","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T01:04:53Z","timestamp":1027645493000},"page":"3-29","source":"Crossref","is-referenced-by-count":105,"title":["Higher-order rewrite systems and their confluence"],"prefix":"10.1016","volume":"192","author":[{"given":"Richard","family":"Mayr","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(97)00143-6_BIB1","article-title":"A general Church-Rosser theorem","author":"Aczel","year":"1978","journal-title":"Tech. Report, Univ. of Manchester"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB2","series-title":"9th IEEE Symp. Logic in Computer Science, IEEE Computer Society Press","first-page":"406","article-title":"Modularity of strong normalization and confluence in the algebraic \u03bb-cube","author":"Barbanera","year":"1994"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB3","series-title":"The Lambda Calculus, its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB4","first-page":"118","article-title":"Lambda calculi with types","volume":"vol. 2","author":"Barendregt","year":"1992"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB5","series-title":"Formal Models and Semantics","first-page":"243","article-title":"Rewrite systems","volume":"vol. B","author":"Dershowitz","year":"1990"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB6","series-title":"Proc. 4th Int. Conf. Rewriting Techniques and Applications","first-page":"34","article-title":"Adding algebraic rewriting to the untyped lambda-calculus","volume":"vol. 488","author":"Dougherty","year":"1991"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB7","series-title":"Logic for Computer Science","author":"Gallier","year":"1986"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB8","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(97)00143-6_BIB9","series-title":"Introduction to HOL: A Theorem-Proving Environment for Higher Order Logic","author":"Gordon","year":"1993"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB10","series-title":"Introduction to Combinators and \u03bb-Calculus","author":"Hindley","year":"1986"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB11","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","article-title":"Confluent reductions: abstract properties and applications to term rewriting systems","volume":"27","author":"Huet","year":"1980","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB12","series-title":"Computational Logic: Essays in Honor of Alan Robinson","first-page":"395","article-title":"Computations in orthogonal rewriting systems","author":"Huet","year":"1991"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB13","series-title":"Rewriting Techniques and Applications","article-title":"Higher-order simplification orderings","author":"Jouannaud","year":"1997"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB14","series-title":"Rewriting Techniques and Applications","first-page":"241","article-title":"Towards a domain theory for termination proofs","volume":"vol. 914","author":"Kahrs","year":"1995"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB15","series-title":"Higher-Order Algebra, Logic, and Term Rewriting","first-page":"109","article-title":"The variable containment problem","volume":"vol. 1074","author":"Kahrs","year":"1996"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB16","article-title":"Combinatory Reduction Systems","volume":"vol. 127","author":"Klop","year":"1980"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB17","first-page":"2","article-title":"Term rewriting systems","volume":"vol. 2","author":"Klop","year":"1992"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","article-title":"Combinatory reduction systems: introduction and survey","volume":"121","author":"Klop","year":"1993","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(97)00143-6_BIB19","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebra","author":"Knuth","year":"1970"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB20","article-title":"A theoretical framework for reasoning about program construction based on extensions of rewrite systems","author":"Lor\u00eda-S\u00e1enz","year":"1993"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB21","series-title":"Rewriting Techniques and Applications","first-page":"26","article-title":"A termination ordering for higher-order rewrite systems","author":"Lysne","year":"1995"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB22","article-title":"Konfluenz bei Termersetzungssystemen auf \u03bb-Termen","author":"Mayr","year":"1994"},{"issue":"4","key":"10.1016\/S0304-3975(97)00143-6_BIB23","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","article-title":"A logic programming language with lambda-abstraction, function variables, and simple unification","volume":"1","author":"Miller","year":"1991","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(97)00143-6_BIB24","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/0020-0190(92)90155-O","article-title":"Confluence of the lambda-calculus with left-linear algebraic rewriting","volume":"41","author":"M\u00fcller","year":"1992","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0304-3975(97)00143-6_BIB25","series-title":"6th IEEE Symp. Logic in Computer Sci., IEEE Computer Soc. Press","first-page":"342","article-title":"Higher-order critical pairs","author":"Nipkow","year":"1991"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB26","series-title":"8th IEEE Symp. Logic in Computer Science, IEEE Computer Soc. Press","first-page":"64","article-title":"Functional unification of higher-order patterns","author":"Nipkow","year":"1993"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB27","series-title":"Proc. Int. Conf. Typed Lambda Calculi and Applications","first-page":"306","article-title":"Orthogonal higher-order rewrite systems are confluent","volume":"vol. 664","author":"Nipkow","year":"1993"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB28","article-title":"Computing in Systems Described by Equations","volume":"vol. 58","author":"O'Donnell","year":"1977"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB29","article-title":"Confluence for abstract and higher-order rewriting","author":"van Oostrom","year":"1994"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB30","series-title":"Higher-Order Algebra, Logic and Term Rewriting","first-page":"276","article-title":"Comparing combinatory reduction systems and higher-order rewrite systems","volume":"vol. 816","author":"van Oostrom","year":"1994"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB31","series-title":"Logical Foundations of Computer Science","first-page":"379","article-title":"Weak orthogonality implies confluence: the higher-order case","volume":"vol. 813","author":"van Oostrom","year":"1994"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB32","series-title":"Typed Lambda Calculi and Applications","first-page":"335","article-title":"On equivalence classes of interpolation equations","volume":"vol. 902","author":"Padovani","year":"1995"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB33","article-title":"Isabelle: A Generic Theorem Prover","volume":"vol. 828","author":"Paulson","year":"1994"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB34","series-title":"Higher-Order Algebra, Logic and Term Rewriting","first-page":"305","article-title":"Termination proofs for higher-order rewrite systems","volume":"vol. 816","author":"van de Pol","year":"1994"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB35","series-title":"Typed Lambda Calculi and Applications","first-page":"350","article-title":"Strict functionals for termination proofs","volume":"vol. 902","author":"van de Pol","year":"1995"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB36","series-title":"Proc. Coll. Trees in Algebra and Programming","first-page":"391","article-title":"Linear unification of higher-order patterns","volume":"vol. 668","author":"Qian","year":"1993"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB37","series-title":"Rewriting Techniques and Applications","first-page":"168","article-title":"Confluence and superdevelopments","volume":"vol. 690","author":"van Raamsdonk","year":"1993"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB38","article-title":"Confluence and normalization for higher-order rewriting","author":"van Raamsdonk","year":"1996"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB39","series-title":"Combinators, \u03bb-Terms, and Proof Theory","author":"Stenlund","year":"1972"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB40","series-title":"Typed Lambda Calculi and Applications","first-page":"406","article-title":"\u03bb-calculi with conditional rules","volume":"vol. 664","author":"Takahashi","year":"1993"},{"key":"10.1016\/S0304-3975(97)00143-6_BIB41","article-title":"The Clausal Theory of Types","volume":"vol. 21","author":"Wolfram","year":"1993"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001436?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001436?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T04:50:07Z","timestamp":1555390207000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397597001436"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,2]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,2]]}},"alternative-id":["S0304397597001436"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(97)00143-6","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1998,2]]}}}