{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:19:22Z","timestamp":1781893162738,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540875307","type":"print"},{"value":"9783540875314","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87531-4_1","type":"book-chapter","created":{"date-parts":[[2008,8,30]],"date-time":"2008-08-30T08:40:53Z","timestamp":1220085653000},"page":"1-14","source":"Crossref","is-referenced-by-count":12,"title":["The Computability Path Ordering: The End of a Quest"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Pierre","family":"Jouannaud","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"4","key":"1_CR1","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1051\/ita:2004015","volume":"38","author":"A. Abel","year":"2004","unstructured":"Abel, A.: Termination checking with types. Theoretical Informatics and Applications\u00a038(4), 277\u2013319 (2004)","journal-title":"Theoretical Informatics and Applications"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Conditional and Typed Rewriting Systems","author":"F. Barbanera","year":"1991","unstructured":"Barbanera, F.: Adding algebraic rewriting to the Calculus of Constructions: strong normalization preserved. In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol.\u00a0516. Springer, Heidelberg (1991)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Typed Lambda Calculi and Applications","author":"F. Barbanera","year":"1993","unstructured":"Barbanera, F., Fern\u00e1ndez, M.: Combining first and higher order rewrite systems with type assignment systems. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664. Springer, Heidelberg (1993)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"F. Barbanera","year":"1993","unstructured":"Barbanera, F., Fern\u00e1ndez, M.: Modularity of termination and confluence in combinations of rewrite systems with \u03bb\n                           \n                    \u03c9\n                  . In: Lingas, A., Carlsson, S., Karlsson, R. (eds.) ICALP 1993. LNCS, vol.\u00a0700. Springer, Heidelberg (1993)"},{"key":"1_CR6","unstructured":"Barbanera, F., Fern\u00e1ndez, M., Geuvers, H.: Modularity of strong normalization and confluence in the algebraic-\u03bb-cube. In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science (1994)"},{"issue":"1","key":"1_CR7","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1017\/S0960129503004122","volume":"14","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Frade, M.J., Gim\u00e9nez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science\u00a014(1), 97\u2013141 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR8","unstructured":"Ben-Amram, A.M., Jones, N.D., Lee, C.S.: The size-change principle for program termination. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (2001)"},{"key":"1_CR9","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions (extended abstract). In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science (2001)"},{"key":"1_CR10","unstructured":"Blanqui, F.: Higher-order dependency pairs. In: Proceedings of the 8th International Workshop on Termination (2006)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721975_4","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2000","unstructured":"Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833. Springer, Heidelberg (2000)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-540-25979-4_2","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2004","unstructured":"Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 24\u201339. Springer, Heidelberg (2004)"},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1017\/S0960129504004426","volume":"15","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science\u00a015(1), 37\u201392 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1-2","key":"1_CR14","first-page":"61","volume":"65","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae\u00a065(1-2), 61\u201386 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-73147-4_4","volume-title":"Rewriting, Computation and Proof","author":"F. Blanqui","year":"2007","unstructured":"Blanqui, F.: Computability closure: Ten years later. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol.\u00a04600, pp. 68\u201388. Springer, Heidelberg (2007)"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0304-3975(00)00347-9","volume":"272","author":"F. Blanqui","year":"2002","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive-data-type Systems. Theoretical Computer Science\u00a0272, 41\u201368 (2002)","journal-title":"Theoretical Computer Science"},{"key":"1_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11916277_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F. Blanqui","year":"2006","unstructured":"Blanqui, F., Jouannaud, J.-P., Rubio, A.: Higher-order termination: from Kruskal to computability. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 1\u201314. Springer, Heidelberg (2006)"},{"key":"1_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-540-75560-9_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F. Blanqui","year":"2007","unstructured":"Blanqui, F., Jouannaud, J.-P., Rubio, A.: HORPO with computability closure: A reconstruction. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 138\u2013150. Springer, Heidelberg (2007)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Rewriting Techniques and Applications","author":"N. Bohr","year":"2004","unstructured":"Bohr, N., Jones, N.: Termination Analysis of the untyped lambda-calculus. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 1\u201323. Springer, Heidelberg (2004)"},{"key":"1_CR20","unstructured":"Borralleras, C.: Ordering-based methods for proving termination automatically. PhD thesis, Universitat Polit\u00e8cnica de Catalunya, Spain (2003)"},{"key":"1_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-8_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Borralleras","year":"2001","unstructured":"Borralleras, C., Rubio, A.: A monotonic higher-order semantic path ordering. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250. Springer, Heidelberg (2001)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-73147-4_2","volume-title":"Rewriting, Computation and Proof","author":"C. Borralleras","year":"2007","unstructured":"Borralleras, C., Rubio, A.: Orderings and constraints: Theory and practice of proving termination. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol.\u00a04600, pp. 28\u201343. Springer, Heidelberg (2007)"},{"key":"1_CR23","unstructured":"Breazu-Tannen, V.: Combining algebra and higher-order types. In: Proceedings of the 3rd IEEE Symposium on Logic in Computer Science (1988)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035757","volume-title":"Automata, Languages and Programming","author":"V. Breazu-Tannen","year":"1989","unstructured":"Breazu-Tannen, V., Gallier, J.: Polymorphic rewriting conserves algebraic strong normalization. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372. Springer, Heidelberg (1989)"},{"issue":"2-3","key":"1_CR25","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/A:1012996816178","volume":"14","author":"W.N. Chin","year":"2001","unstructured":"Chin, W.N., Khoo, S.C.: Calculating sized types. Journal of Higher-Order and Symbolic Computation\u00a014(2-3), 261\u2013300 (2001)","journal-title":"Journal of Higher-Order and Symbolic Computation"},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term rewriting systems. Theoretical Computer Science\u00a017, 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"key":"1_CR27","unstructured":"Dershowitz, N.: Personal Communication (2008)"},{"issue":"2","key":"1_CR28","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","volume":"101","author":"D. Dougherty","year":"1992","unstructured":"Dougherty, D.: Adding algebraic rewriting to the untyped lambda calculus. Information and Computation\u00a0101(2), 251\u2013267 (1992)","journal-title":"Information and Computation"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/11805618_23","volume-title":"Term Rewriting and Applications","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Swiderski, S., Schneider-Kamp, P., Thiemann, R.: Automated termination analysis for haskell: From term rewriting to programming languages. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 297\u2013312. Springer, Heidelberg (2006)"},{"key":"1_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_34","volume-title":"Computer Science Logic","author":"J. Goubault-Larrecq","year":"2001","unstructured":"Goubault-Larrecq, J.: Well-founded recursive relations. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142. Springer, Heidelberg (2001)"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proceedings of the 23th ACM Symposium on Principles of Programming Languages (1996)","DOI":"10.1145\/237721.240882"},{"issue":"6","key":"1_CR33","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1145\/1034774.1034775","volume":"26","author":"C.B. Jay","year":"2004","unstructured":"Jay, C.B.: The pattern calculus. ACM Transactions on Programming Languages and Systems\u00a026(6), 911\u2013937 (2004)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR34","unstructured":"Jouannaud, J.-P., Okada, M.: A computation model for executable higher-order algebraic specification languages. In: Proceedings of the 6th IEEE Symposium on Logic in Computer Science (1991)"},{"issue":"2","key":"1_CR35","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/S0304-3975(96)00161-2","volume":"173","author":"J.-P. Jouannaud","year":"1997","unstructured":"Jouannaud, J.-P., Okada, M.: Abstract Data Type Systems. Theoretical Computer Science\u00a0173(2), 349\u2013391 (1997)","journal-title":"Theoretical Computer Science"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/11805618_29","volume-title":"Term Rewriting and Applications","author":"J.-P. Jouannaud","year":"2006","unstructured":"Jouannaud, J.-P., Rubio, A.: Higher-order orderings for normal rewriting. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 387\u2013399. Springer, Heidelberg (2006)"},{"key":"1_CR37","unstructured":"Jouannaud, J.-P., Rubio, A.: The Higher-Order Recursive Path Ordering. In: Proceedings of the 14th IEEE Symposium on Logic in Computer Science (1999)"},{"key":"1_CR38","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0304-3975(98)00078-4","volume":"208","author":"J.-P. Jouannaud","year":"1998","unstructured":"Jouannaud, J.-P., Rubio, A.: Rewrite orderings for higher-order terms in eta-long beta-normal form and the recursive path ordering. Theoretical Computer Science\u00a0208, 33\u201358 (1998)","journal-title":"Theoretical Computer Science"},{"key":"1_CR39","unstructured":"Jouannaud, J.-P., Rubio, A.: Higher-order recursive path orderings \u201c\u00e0 la carte\u201d, Draft (2001)"},{"issue":"1","key":"1_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1206035.1206037","volume":"54","author":"J.-P. Jouannaud","year":"2007","unstructured":"Jouannaud, J.-P., Rubio, A.: Polymorphic higher-order recursive path orderings. Journal of the ACM\u00a054(1), 1\u201348 (2007)","journal-title":"Journal of the ACM"},{"key":"1_CR41","unstructured":"Kamin, S., L\u00e9vy, J.-J.: Two generalizations of the Recursive Path Ordering (unpublished, 1980)"},{"issue":"2-3","key":"1_CR42","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"M.S. Krishnamoorthy","year":"1985","unstructured":"Krishnamoorthy, M.S., Narendran, P.: On recursive path ordering. Theoretical Computer Science\u00a040(2-3), 323\u2013328 (1985)","journal-title":"Theoretical Computer Science"},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","volume-title":"Conditional Term Rewriting Systems","author":"C. Loria-Saenz","year":"1993","unstructured":"Loria-Saenz, C., Steinbach, J.: Termination of combined (rewrite and \u03bb-calculus) systems. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656. Springer, Heidelberg (1993)"},{"key":"1_CR44","volume-title":"Proceedings of the 1989 International Symposium on Symbolic and Algebraic Computation","author":"M. Okada","year":"1989","unstructured":"Okada, M.: Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In: Proceedings of the 1989 International Symposium on Symbolic and Algebraic Computation. ACM Press, New York (1989)"},{"issue":"3","key":"1_CR45","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1093\/ietisy\/e88-d.3.583","volume":"E88-D","author":"M. Sakai","year":"2005","unstructured":"Sakai, M., Kusakari, K.: On dependency pair method for proving termination of higher-order rewrite systems. IEICE Transactions on Information and Systems\u00a0E88-D(3), 583\u2013593 (2005)","journal-title":"IEICE Transactions on Information and Systems"},{"issue":"8","key":"1_CR46","first-page":"1025","volume":"E84-D","author":"M. Sakai","year":"2001","unstructured":"Sakai, M., Watanabe, Y., Sakabe, T.: An extension of dependency pair method for proving termination of higher-order rewrite systems. IEICE Transactions on Information and Systems\u00a0E84-D(8), 1025\u20131032 (2001)","journal-title":"IEICE Transactions on Information and Systems"},{"key":"1_CR47","series-title":"Lecture Notes in Computer Science","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"J. van de Pol","year":"1994","unstructured":"van de Pol, J.: Termination proofs for higher-order rewrite systems. In: Heering, J., Meinke, K., M\u00f6ller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol.\u00a0816. Springer, Heidelberg (1994)"},{"key":"1_CR48","unstructured":"van de Pol, J.: Termination of higher-order rewrite systems. PhD thesis, Utrecht Universiteit, Nederlands (1996)"},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014064","volume-title":"Typed Lambda Calculi and Applications","author":"J. van de Pol","year":"1995","unstructured":"van de Pol, J., Schwichtenberg, H.: Strict functionals for termination proofs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902. Springer, Heidelberg (1995)"},{"key":"1_CR50","unstructured":"van Raamsdong, F., Kop, C.: Personal Communication (2008)"},{"issue":"2","key":"1_CR51","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1017\/S0956796802004641","volume":"13","author":"D. Walukiewicz-Chrzaszcz","year":"2003","unstructured":"Walukiewicz-Chrzaszcz, D.: Termination of rewriting in the Calculus of Constructions. Journal of Functional Programming\u00a013(2), 339\u2013414 (2003)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"1_CR52","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"H. Xi","year":"2002","unstructured":"Xi, H.: Dependent types for program termination verification. Journal of Higher-Order and Symbolic Computation\u00a015(1), 91\u2013131 (2002)","journal-title":"Journal of Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87531-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:12:03Z","timestamp":1715058723000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-87531-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540875307","9783540875314"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87531-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}