{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:54:31Z","timestamp":1781927671483,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540421177","type":"print"},{"value":"9783540451273","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45127-7_20","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:25:25Z","timestamp":1184588725000},"page":"261-275","source":"Crossref","is-referenced-by-count":11,"title":["On Termination of Higher-Order Rewriting"],"prefix":"10.1007","author":[{"given":"Femke","family":"van Raamsdonk","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,5,8]]},"reference":[{"issue":"6","key":"20_CR1","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1017\/S095679689700289X","volume":"7","author":"F. Barbanera","year":"1997","unstructured":"F. Barbanera, M. Fern\u00e1ndez, and H. Geuvers. Modularity of strong normalization in the algebraic lambda-cube. Jounal of Functional Programming, 7(6):613\u2013660, 1997. An earlier version appears in the Proceedings of LICS\u2019 94.","journal-title":"Jounal of Functional Programming"},{"key":"20_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/10721975_4","volume-title":"Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA\u2019 99)","author":"F. Blanqui","year":"2000","unstructured":"F. Blanqui. Termination and con uence of higher-order rewrite systems. In L. Bachmair, editor, Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA\u2019 99), number 1833 in LNCS, pages 47\u201362, Norwich, UK, July 2000. Springer Verlag."},{"issue":"3","key":"20_CR3","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":"20_CR4","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and M. Okada. A computation model for executable higher-order algebraic specification languages. In Proceedings of the 6th annual IEEE Symposium on Logic in Computer Science (LICS\u2019 91), pages 350\u2013361, Amsterdam, The Netherlands, July 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"20_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/3-540-61464-8_46","volume-title":"Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA\u2019 96)","author":"J.-P. Jouannaud","year":"1996","unstructured":"J.-P. Jouannaud and A. Rubio. A recursive path ordering for higher-order terms in \u03b7-long \u03b2-normal form. In H. Gantzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA\u2019 96), number 1103 in LNCS, pages 108\u2013122, New Brunswick, USA, July 1996. Springer Verlag."},{"key":"20_CR6","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), pages 402\u2013411, Trento, Italy, July 1999.","DOI":"10.1109\/LICS.1999.782635"},{"key":"20_CR7","unstructured":"J.-P. Jouannaud and A. Rubio. Higher-order recursive path orderings \u00e0 la carte. \n                    http:\/\/www.lri.fr\/~jouannau\/biblio.html\n                    \n                  , 2000."},{"key":"20_CR8","series-title":"Mathematical Centre Tracts","volume-title":"Combinatory Reduction Systems","author":"J.W. Klop","year":"1980","unstructured":"J.W. Klop. Combinatory Reduction Systems. Number 127 in Mathematical Centre Tracts. CWI, Amsterdam, The Netherlands, 1980. PhD Thesis."},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory Reduction Systems: introduction and survey. Theoretical Computer Science, 121:279\u2013308, 1993. Special issue in honour of Corrado B\u00f6hm.","journal-title":"Theoretical Computer Science"},{"key":"20_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-56393-8_10","volume-title":"Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems (CTRS\u201992)","author":"C. Loria-Saenz","year":"1993","unstructured":"C. Loria-Saenz and J. Steinbach. Termination of combined (rewrite and lambda-calculus) systems. In M. Rusinowitch and J.-L. R\u00e9my, editors, Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems (CTRS\u201992), number 656 in LNCS, pages 143\u2013147, Pont-\u00e0-Mousson, France, April 1993. Springer Verlag."},{"key":"20_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/3-540-59200-8_45","volume-title":"Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA\u2019 95)","author":"O. Lysne","year":"1995","unstructured":"O. Lysne and J. Piris. A termination ordering for higher order rewrite systems. In J. Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA\u2019 95), number 914 in LNCS, pages 26\u201340, Kaiserslautern, Germany, April 1995. Springer Verlag."},{"key":"20_CR12","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"},{"issue":"4","key":"20_CR13","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":"20_CR14","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":"20_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"392","DOI":"10.1007\/3-540-61464-8_67","volume-title":"Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA\u2019 96)","author":"V. Oostrom van","year":"1996","unstructured":"V. van Oostrom. Higher-order families. In H. Gantzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA\u2019 96), number 1103 in LNCS, pages 392\u2013407, New Brunswick, USA, July 1996. Springer Verlag."},{"key":"20_CR16","volume-title":"Termination of higher-order rewrite systems","author":"J.C. Pol van de","year":"1996","unstructured":"J.C. van de Pol. Termination of higher-order rewrite systems. PhD thesis, Utrecht University, Utrecht, The Netherlands, December 1996."},{"key":"20_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/3-540-48685-2_17","volume-title":"Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA\u2019 99)","author":"F. Raamsdonk van","year":"1999","unstructured":"F. van Raamsdonk. Higher-order rewriting. In P. Narendran and M. Rusinowitch, editors, Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA\u2019 99), number 1631 in LNCS, pages 220\u2013239, Trento, Italy, July 1999. Springer Verlag."}],"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-45127-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T20:48:36Z","timestamp":1550436516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45127-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421177","9783540451273"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45127-7_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}