{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:38:38Z","timestamp":1725489518556},"publisher-location":"Berlin, Heidelberg","reference-count":51,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540731467"},{"type":"electronic","value":"9783540731474"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"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":[[2007]]},"DOI":"10.1007\/978-3-540-73147-4_4","type":"book-chapter","created":{"date-parts":[[2007,8,17]],"date-time":"2007-08-17T00:01:50Z","timestamp":1187308910000},"page":"68-88","source":"Crossref","is-referenced-by-count":4,"title":["Computability Closure: Ten Years Later"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","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":"4_CR2","volume-title":"Handbook of logic in computer science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of logic in computer science, vol.\u00a02, Oxford University Press, Oxford, UK (1992)"},{"key":"4_CR3","unstructured":"Blanqui, F.: Higher-order dependency pairs. In: Proceedings of the 8th International Workshop on Termination (2006)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44881-0_28","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2003","unstructured":"Blanqui, F.: Rewriting modulo in Deduction modulo. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, Springer, Heidelberg (2003)"},{"key":"4_CR5","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)"},{"issue":"1","key":"4_CR6","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"},{"key":"4_CR7","unstructured":"Blanqui, F.: (HO) RPO revisited. Research Report 5972, INRIA (2006)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","first-page":"4","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"1999","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: The Calculus of Algebraic Constructions. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, Springer, Heidelberg (1999)"},{"key":"4_CR9","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":"4_CR10","unstructured":"Breazu-Tannen,V.: Combining algebra and higher-order types. In: Proceedings of the 3rd IEEE Symposium on Logic in Computer Science (1988)"},{"key":"4_CR11","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: Della Rocca, S.R., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989, LNCS, vol.\u00a0372, Springer, Heidelberg (1989)"},{"issue":"1","key":"4_CR12","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(91)90037-3","volume":"83","author":"V. Breazu-Tannen","year":"1991","unstructured":"Breazu-Tannen, V., Gallier, J.: Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science\u00a083(1), 3\u201328 (1991)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"4_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1078","volume":"114","author":"V. Breazu-Tannen","year":"1994","unstructured":"Breazu-Tannen, V., Gallier, J.: Polymorphic rewriting conserves algebraic confluence. Information and Computation\u00a0114(1), 1\u201329 (1994)","journal-title":"Information and Computation"},{"key":"4_CR14","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":"4_CR15","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, ch.6. North-Holland, Amsterdam (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"D. Dougherty","year":"1991","unstructured":"Dougherty, D.: Adding algebraic rewriting to the untyped lambda calculus. In: Book, R.V. (ed.) RTA 1996, LNCS, vol.\u00a0488, Springer, Heidelberg (1991)"},{"issue":"2","key":"4_CR17","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":"4_CR18","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Une extension de l\u2019interpr\u00e9tation de G\u00f6del \u00e0 l\u2019analyse et son application \u00e0 l\u2019\u00e9limination des coupures dans l\u2019analyse et la th\u00e9orie des types. In: Fenstad, J. (ed) Proc. of the 2nd Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol.\u00a063. North-Holland, Amsterdam (1971)","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"4_CR19","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l\u2019arithmetique d\u2019ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, France (1972)"},{"key":"4_CR20","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1988","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge University Press, Cambridge (1988)"},{"issue":"4","key":"4_CR21","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal on Computing\u00a015(4), 1155\u20131194 (1986)","journal-title":"SIAM Journal on Computing"},{"key":"4_CR22","unstructured":"Jouannaud, J.-P., Okada, M.: Executable higher-order algebraic specification languages. In: Proceedings of the 6th IEEE Symposium on Logic in Computer Science (1991)"},{"issue":"2","key":"4_CR23","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":"4_CR24","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2006)"},{"key":"4_CR25","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":"4_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"RTA 1996","author":"J.-P. Jouannaud","year":"1996","unstructured":"Jouannaud, J.-P., Rubio, A.: A recursive path ordering for higher-order terms in eta-long beta-normal form. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, Springer, Heidelberg (1996)"},{"key":"4_CR27","unstructured":"Khasidashvili, Z.: Expression Reduction Systems. In: Proc. of I. Vekua Institute of Applied Mathematics, vol.\u00a036 (1990)"},{"key":"4_CR28","unstructured":"Klop, J.\u00a0W.: Combinatory Reduction Systems PhD thesis, Utrecht Universiteit, The Netherlands, Published as Mathematical Center Tract 129 (1980)"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science\u00a0121, 279\u2013308 (1993)","journal-title":"Theoretical Computer Science"},{"key":"4_CR30","doi-asserted-by":"publisher","first-page":"210","DOI":"10.2307\/1993287","volume":"95","author":"J.B. Kruskal","year":"1960","unstructured":"Kruskal, J.B.: Well-quasi-ordering, the tree theorem, and vazsonyi\u2019s conjecture. Transactions of the American Mathematical Society\u00a095, 210\u2013225 (1960)","journal-title":"Transactions of the American Mathematical Society"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Conditional Term Rewriting Systems","author":"C. Loria-Saenz","year":"1992","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 (1992)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"O. Lysne","year":"1995","unstructured":"Lysne, O., Piris, J.: A termination ordering for higher order rewrite systems. In: Hsiang, J. (ed.) RTA 1995, LNCS, vol.\u00a0914, Springer, Heidelberg (1995)"},{"issue":"2","key":"4_CR33","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science\u00a0192(2), 3\u201329 (1998)","journal-title":"Theoretical Computer Science"},{"key":"4_CR34","unstructured":"Mendler, N.\u00a0P.: Recursive types and type constraints in second order lambda calculus. In: Proceedings of the 2nd IEEE Symposium on Logic in Computer Science (1987)"},{"issue":"1-2","key":"4_CR35","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"N.P. Mendler","year":"1991","unstructured":"Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic\u00a051(1-2), 159\u2013172 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","volume-title":"Extensions of Logic Programming","author":"D. Miller","year":"1989","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Schroeder-Heister, P. (ed.) ELP 1989, LNCS, vol.\u00a0475, Springer, Heidelberg (1989)"},{"issue":"4","key":"4_CR37","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation\u00a01(4), 497\u2013536 (1991)","journal-title":"Journal of Logic and Computation"},{"volume-title":"An overview of \u03bbProlog.","year":"1988","key":"4_CR38","unstructured":"Miller, D., Nadathur, G.: An overview of \u03bbProlog. In: Proceedings of the 5th International Conference on Logic Programming. MIT Press, Cambridge, MA (1988)"},{"key":"4_CR39","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proceedings of the 6th IEEE Symposium on Logic in Computer Science (1991)"},{"key":"4_CR40","doi-asserted-by":"crossref","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)","DOI":"10.1145\/74540.74582"},{"key":"4_CR41","unstructured":"Plaisted, D.A.: A recursively defined ordering for proving termination of term rewriting systems. Technical report, University of Illinois, Urbana-Champaign, United States (1978)"},{"key":"4_CR42","unstructured":"Sakai, M., Kusakari, K.: On new dependency pair method for proving termination of higher-order rewrite systems. In: Proceedings of the 1st International Workshop on Rewriting in Proof and Computation (2001)"},{"issue":"2","key":"4_CR43","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic\u00a032(2), 198\u2013212 (1967)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Tait, W.W.: A realizability interpretation of the theory of species. In: Parikh, R. (eds.) Proceedings of the 1972 Logic Colloquium. Lecture Notes in Mathematics, vol.\u00a0453. Springer, Heidelberg (1975)","DOI":"10.1007\/BFb0064875"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"J. Pol van de","year":"1993","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 (1993)"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"V. Oostrom van","year":"1995","unstructured":"van Oostrom, V.: Development closed critical pairs. In: Dowek, G., Heering, J., Meinke, K., M\u00f6ller, B. (eds.) HOA 1995. LNCS, vol.\u00a01074, Springer, Heidelberg (1995)"},{"key":"4_CR47","unstructured":"van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit Amsterdam, The Netherlands (1994)"},{"issue":"2","key":"4_CR48","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson, G., Stickel, M.: Complete sets of reductions for some equational theories. Journal of the ACM\u00a028(2), 233\u2013264 (1981)","journal-title":"Journal of the ACM"},{"key":"4_CR49","unstructured":"van Raamsdonk, F.: Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Vrije University Amsterdam, The Netherlands (1996)"},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"Walukiewicz-Chrz\u0105szcz, D.: Termination of Rewriting in the Calculus of Constructions. PhD thesis, Warsaw University, Poland and Universit\u00e9 d\u2019Orsay, France (2003)","DOI":"10.1017\/S0956796802004641"},{"issue":"2","key":"4_CR51","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1017\/S0956796802004641","volume":"13","author":"D. Walukiewicz-Chrz\u0105szcz","year":"2003","unstructured":"Walukiewicz-Chrz\u0105szcz, D.: Termination of rewriting in the Calculus of Constructions. Journal of Functional Programming\u00a013(2), 339\u2013414 (2003)","journal-title":"Journal of Functional Programming"}],"container-title":["Lecture Notes in Computer Science","Rewriting, Computation and Proof"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73147-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T20:59:32Z","timestamp":1558472372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73147-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540731467","9783540731474"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73147-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}