{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:22Z","timestamp":1775873542866,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662013","type":"print"},{"value":"9783540486855","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48685-2_17","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:41Z","timestamp":1269882821000},"page":"220-239","source":"Crossref","is-referenced-by-count":11,"title":["Higher-Order Rewriting"],"prefix":"10.1007","author":[{"given":"Femke","family":"van Raamsdonk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,11,5]]},"reference":[{"key":"17_CR1","unstructured":"P. Aczel. A general Church-Rosser theorem. University of Manchester, July 1978."},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1017\/S0960129500000566","volume":"4","author":"A. Asperti","year":"1994","unstructured":"A. Asperti and C. Laneve. Interaction systems I: The theory of optimal reductions. Mathematical Structures in Computer Science, 4:457\u2013504, 1994.","journal-title":"Mathematical Structures in Computer Science"},{"key":"17_CR3","unstructured":"H.P. Barendregt. The Lambda Calculus, its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, revised edition, 1984."},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(86)90033-4","volume":"32","author":"J.A. Bergstra","year":"1986","unstructured":"J.A. Bergstra and J.W. Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32:323\u2013362, 1986.","journal-title":"Journal of Computer and System Sciences"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"472","DOI":"10.2307\/1989762","volume":"39","author":"A. Church","year":"1936","unstructured":"Alonzo Church and J.B. Rosser. Some properties of conversion. Transactions of the Americal Mathematical Society, 39:472\u2013482, 1936.","journal-title":"Transactions of the Americal Mathematical Society"},{"issue":"3","key":"17_CR6","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term rewriting systems. Theoretical Computer Science, 17(3):279\u2013301, 1982.","journal-title":"Theoretical Computer Science"},{"key":"17_CR7","unstructured":"R.O. Gandy. Proofs of strong normalization. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457\u2013477. Academic Press, 1980."},{"key":"17_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-61064-2_37","volume-title":"Proceedings of the 19th International Colloquium on Trees in Algebras and Programming (CAAP\u2019 96)","author":"J. Glauert","year":"1996","unstructured":"J. Glauert and Z. Khasidashvili. Relative normalization in deterministic residual structures. In Proceedings of the 19th International Colloquium on Trees in Algebras and Programming (CAAP\u2019 96), volume 1059 of Lecture Notes in Computer Science, pages 180\u2013195, April 1996."},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/3-540-61464-8_48","volume-title":"Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA\u2019 96)","author":"M. Hanus","year":"1996","unstructured":"M. Hanus and C. Prehofer. Higher-order narrowing with definitional trees. In H. Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA\u2019 96), volume 1103 of Lecture Notes in Computer Science, pages 138\u2013152, New Brunswick, USA, 1996."},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/1998825","volume":"240","author":"R. Hindley","year":"1978","unstructured":"R. Hindley. Reductions of residuals are finite. Transactions of the Americal Mathematical Society, 240:345\u2013361, June 1978.","journal-title":"Transactions of the Americal Mathematical Society"},{"issue":"4","key":"17_CR11","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 rewriting systems. Journal of the Association for Computing Machinery, 27(4):797\u2013821, October 1980.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"G. Huet and D.C. Oppen. Equations and rewrite rules, a survey. In R.V. Book, editor, Formal Language Theory, Perspectives and Open Problems, pages 349\u2013405. Academic Press, 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proceedings of the 14th annual IEEE Symposium on Logic in Computer Science (LICS\u2019 99), Trento, Italy, 1999. To appear.","DOI":"10.1109\/LICS.1999.782635"},{"key":"17_CR14","unstructured":"S. Kahrs. Termination proofs in an abstract setting. To appear in Mathematical Structures in Computer Science."},{"key":"17_CR15","first-page":"200","volume":"36","author":"Z.O. Khasidashvili","year":"1990","unstructured":"Z.O. Khasidashvili. Expression Reduction Systems. In Proceedings of I. Vekua Institute of Applied Mathematics, volume 36, pages 200\u2013220, Tblisi, 1990.","journal-title":"Proceedings of I. Vekua Institute of Applied Mathematics"},{"key":"17_CR16","volume-title":"Mathematical Centre Tracts","author":"J.W. Klop","year":"1980","unstructured":"J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. CWI, Amsterdam, 1980. PhD Thesis."},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3\u201329, 1998.","journal-title":"Theoretical Computer Science"},{"key":"17_CR19","unstructured":"P.-A. Melli\u00e8s. Description Abstraite des Syst\u00e9mes de R\u00e9\u00e9criture. PhD thesis, Universit\u00e9 de Paris VII, Paris, France, 1996."},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"A. Middeldorp. Call by need computations to root-stable form. In Proceedings of the 24th Symposium on Principles of Programming Languages (POPL\u2019 97), pages 94\u2013105, Paris, France, January 1997. ACM Press.","DOI":"10.1145\/263699.263711"},{"issue":"4","key":"17_CR21","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497\u2013536, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS\u2019 91), pages 342\u2013349, Amsterdam, The Netherlands, July 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"17_CR23","unstructured":"T. Nipkow and C. Prehofer. Higher-order rewriting and equational reasoning. In W. Bibel and P. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications. Volume I: Foundations, volume 8 of Applied Logic Series, pages 399\u2013430. Kluwer, 1998."},{"key":"17_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08531-9","volume-title":"Computing in Systems Described by Equations","author":"M.J. O\u2019Donnell","year":"1977","unstructured":"M.J. O\u2019Donnell. Computing in Systems Described by Equations, volume 58 of Lecture Notes in Computer Science. Springer Verlag, 1977."},{"key":"17_CR25","unstructured":"V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhDthesis, Vrije Universiteit, Amsterdam, The Netherlands, March 1994."},{"issue":"1","key":"17_CR26","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/S0304-3975(96)00173-9","volume":"175","author":"V. Oostrom van","year":"1997","unstructured":"V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159\u2013181, 1997.","journal-title":"Theoretical Computer Science"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"V. van Oostrom. Normalisation in weakly orthogonal rewriting. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA\u2019 99), 1999.","DOI":"10.1007\/3-540-48685-2_5"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48685-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:01:39Z","timestamp":1558969299000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48685-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662013","9783540486855"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-48685-2_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}