{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:24:49Z","timestamp":1745994289034},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2007,7,11]],"date-time":"2007-07-11T00:00:00Z","timestamp":1184112000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AAECC"],"published-print":{"date-parts":[[2007,9,25]]},"DOI":"10.1007\/s00200-007-0046-9","type":"journal-article","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T22:47:20Z","timestamp":1184626040000},"page":"407-431","source":"Crossref","is-referenced-by-count":12,"title":["Enhancing dependency pair method using strong computability in simply-typed term rewriting"],"prefix":"10.1007","volume":"18","author":[{"given":"Keiichirou","family":"Kusakari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masahiko","family":"Sakai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,7,11]]},"reference":[{"key":"46_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, H., Khoo, S.C.: Affine-based size-change termination. In: Proceedings of the 1st Asign Symposium. On Programming Languages and Systems, LNCS 2895 (APLAS2003), pp. 122\u2013140 (2003)","DOI":"10.1007\/978-3-540-40018-9_9"},{"key":"46_CR2","doi-asserted-by":"crossref","unstructured":"Aoto, T., Yamada, T.: Dependency pairs for simply typed term rewriting. In: Proceedings of the 16th International Conference On Rewriting Techniques and Applications, LNCS 3467 (RTA2005), pp. 120\u2013134 (2005)","DOI":"10.1007\/978-3-540-32033-3_10"},{"key":"46_CR3","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts T. and Giesl J. (2000). Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236: 133\u2013178","journal-title":"Theor. Comput. Sci."},{"key":"46_CR4","doi-asserted-by":"crossref","unstructured":"Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Proceedings of the 11th International Conference On Rewriting Techniques and Applications, LNCS 1833 (RTA2000), pp. 47\u201361 (2000)","DOI":"10.1007\/10721975_4"},{"key":"46_CR5","unstructured":"Blanqui, F.: Higher-order dependency pairs. In: Proceedings of the 8th International Workshop on Termination (WST06), pp. 22\u201326 (2006)"},{"issue":"3","key":"46_CR6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz N. (1982). Orderings for term-rewriting systems. Theor. Comput. Sci 17(3): 279\u2013301","journal-title":"Theor. Comput. Sci"},{"key":"46_CR7","unstructured":"Dershowitz, N.: Termination dependencies. In: Proceedings of the 6th International Workshop on Termination (WST03), pp. 27\u201330 (2003)"},{"issue":"1","key":"46_CR8","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl J., Arts T. and Ohlebusch E. (2002). Modular termination proofs for rewriting using dependency pairs. J. Sym. Comput. 34(1): 21\u201358","journal-title":"J. Sym. Comput."},{"key":"46_CR9","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LNAI 2850 (LPAR2003), pp. 165\u2013179 (2003)"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: Proceedings of the 15th International Conference On Rewriting Techniques and Applications, LNCS 3091 (RTA2004), pp. 210\u2013220 (2004)","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LNCS 3452 (LPAR2004), pp. 301\u2013331 (2005)","DOI":"10.1007\/978-3-540-32275-7_21"},{"key":"46_CR12","doi-asserted-by":"crossref","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Proceedings the 5th International. Workshop on Frontiers of Combining Systems LNAI 3717 (FroCoS\u201905), pp. 216\u2013231 (2005)","DOI":"10.1007\/11559306_12"},{"key":"46_CR13","unstructured":"Girard, J.-Y.: Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph.D. thesis, University of Paris VII (1972)"},{"key":"46_CR14","first-page":"309","volume-title":"Research Topics in Functional Programming","author":"J.A. Goguen","year":"1990","unstructured":"Goguen, J.A.: Higher-order functions considered unnecessary for higher-order programming. In: Truner, D.A. (ed.) Research Topics in Functional Programming. Addison-Wesley Longman Publishing, Reading, pp. 309\u2013351 (1990)"},{"key":"46_CR15","volume-title":"Introduction to Combinators and \u03bb-Calculus","author":"J.R. Hindley","year":"1986","unstructured":"Hindley J.R. and Seldin J.P. (1986). Introduction to Combinators and \u03bb-Calculus. Cambridge University Press, Cambridge"},{"key":"46_CR16","doi-asserted-by":"crossref","unstructured":"Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: Proceedings of the 15th International Conference On Rewriting Techniques and Applications, LNCS 3091 (RTA04), pp. 249\u2013268 (2004)","DOI":"10.1007\/978-3-540-25979-4_18"},{"key":"46_CR17","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Rubio, A.: The higher-order recursive path ordering. In: Proceedings of 14th Annual IEEE Symposium on Logic in Computer Science, IEEE Comp. Sci. Press, New York, pp. 402\u2013411","DOI":"10.1109\/LICS.1999.782635"},{"issue":"1","key":"46_CR18","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1006\/jsco.1996.0002","volume":"21","author":"R. Kennaway","year":"1996","unstructured":"Kennaway R., Klop J.W., Sleep M.R. and Vries F.J. (1996). Comparing curried and uncurried rewriting. J. Sym. Comput. 21(1): 15\u201339","journal-title":"J. Sym. Comput."},{"key":"46_CR19","doi-asserted-by":"crossref","unstructured":"Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Proceedings of International Conference On Principles and Practice of Declarative Programming, LNCS 1702 (PPDP\u201999), pp. 47\u201361 (1999)","DOI":"10.1007\/10704567_3"},{"key":"46_CR20","unstructured":"Kusakari, K.: On proving termination of term rewriting systems with higher-order variables. In: IPSJ Transactions on Programming, vol. 42, no.SIG 7 (PRO 11), pp. 35\u201345 (2001)"},{"issue":"2","key":"46_CR21","first-page":"352","volume":"E87-D","author":"K. Kusakari","year":"2004","unstructured":"Kusakari K. (2004). Higher-order path orders based on computability. IEICE Trans. Inform. Syst. E E87-D(2): 352\u2013359","journal-title":"IEICE Trans. Inform. Syst. E"},{"issue":"12","key":"46_CR22","doi-asserted-by":"crossref","first-page":"2715","DOI":"10.1093\/ietisy\/e88-d.12.2715","volume":"E88-D","author":"K. Kusakari","year":"2005","unstructured":"Kusakari K., Sakai M. and Sakabe T. (2005). Primitive inductive theorems bridge implicit induction methods and inductive theorems in higher-order rewriting. IEICE Trans. Inform. Syst. E E88-D(12): 2715\u20132726","journal-title":"IEICE Trans. Inform. Syst. E"},{"issue":"4","key":"46_CR23","doi-asserted-by":"crossref","first-page":"707","DOI":"10.1093\/ietisy\/e90-d.4.707","volume":"E90-D","author":"K. Kusakari","year":"2007","unstructured":"Kusakari K. and Chiba Y. (2007). A higher-order Knuth\u2013Bendix procedure and its applications. IEICE Trans. Inform. Syst. E E90-D(4): 707\u2013715","journal-title":"IEICE Trans. Inform. Syst. E"},{"key":"46_CR24","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of the 28th ACM Symposium. On Principles of Programming Languages (POPL2001), pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"46_CR25","doi-asserted-by":"crossref","first-page":"873","DOI":"10.1016\/j.jsc.2004.02.003","volume":"38","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9 C. and Urbain X. (2004). Modular and incremental proofs of AC-termination. J. Sym. Comput. 38: 873\u2013897","journal-title":"J. Sym. Comput."},{"key":"46_CR26","doi-asserted-by":"crossref","unstructured":"Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Proceedings of the International Joint Conference on Automated Reasoning, LNAI 2083 (IJCAR01), pp. 593\u2013610 (2001)","DOI":"10.1007\/3-540-45744-5_49"},{"key":"46_CR27","doi-asserted-by":"crossref","unstructured":"Van Raamsdonk, F.: On termination of higher-order rewriting. In: Proceedings of 12th International Conference On Rewriting Techniques and Applications, LNCS 2051 (RTA2001), pp. 261\u2013275 (2001)","DOI":"10.1007\/3-540-45127-7_20"},{"issue":"4","key":"46_CR28","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1023\/A:1010027404223","volume":"11","author":"J. Reynolds","year":"1998","unstructured":"Reynolds J. (1998). Definitional interpreters for higher-order programming languages. Higher Order Computation 11(4): 363\u2013397(1998) Reprinted from the Proceedings of the 25th ACM National Conference (1972)","journal-title":"Higher Order Computation"},{"issue":"8","key":"46_CR29","first-page":"1025","volume":"E84-D","author":"M. Sakai","year":"2001","unstructured":"Sakai M., Watanabe Y. and Sakabe T. (2001). Dependency pair method for proving termination of higher-order rewrite systems. IEICE Trans. Inform. Syst. E E84-D(8): 1025\u20131032","journal-title":"IEICE Trans. Inform. Syst. E"},{"issue":"3","key":"46_CR30","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1093\/ietisy\/e88-d.3.583","volume":"E88-D","author":"M. Sakai","year":"2005","unstructured":"Sakai M. and Kusakari K. (2005). On dependency pair method for proving termination of higher-order rewrite systems. IEICE Trans. Inform. Syst. E E88-D(3): 583\u2013593","journal-title":"IEICE Trans. Inform. Syst. E"},{"issue":"4","key":"46_CR31","first-page":"978","volume":"J90-D","author":"T. Sakurai","year":"2007","unstructured":"Sakurai T., Kusakari K., Sakai M., Sakabe T. and Nishida N. (2007). Usable rules and labeling product-typed terms for dependency pair method in simply-typed term rewriting systems. IEICE Trans. Inform. Syst. J J90-D(4): 978\u2013989","journal-title":"IEICE Trans. Inform. Syst. J"},{"key":"46_CR32","unstructured":"Sakurai, T., Kusakari, K., Nishida, N., Sakai, M., Sakabe, T.: Proving sufficient completeness of functional programs based on recursive structure analysis and strong computability. In: Proceedings of the Forum on Information Technology 2005 (FIT2005), Information Technology Letters, LA-001, pp. 1\u20134, 2005 (in Japanese)"},{"key":"46_CR33","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"T.T. Tait","year":"1967","unstructured":"Tait T.T. (1967). Intensional interpretation of functionals of finite type. J. Symbolic Logic 32: 198\u2013212","journal-title":"J. Symbolic Logic"},{"key":"46_CR34","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)"},{"key":"46_CR35","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proceedings of the 2nd International Joint Conference on Automated Reasoning, LNAI 3097 (IJCAR2004), pp. 75\u201390 (2004)","DOI":"10.1007\/978-3-540-25984-8_4"},{"issue":"4","key":"46_CR36","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/s00200-005-0179-7","volume":"16","author":"R. Thiemann","year":"2005","unstructured":"Thiemann R. and Giesl J. (2005). The size-change principle and dependency pairs for termination of term rewriting. Appl. Algebra Eng. Commun. Comput. 16(4): 229\u2013270","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"46_CR37","doi-asserted-by":"crossref","unstructured":"Toyama, Y.: Termination of S-expression rewriting systems: lexicographic path ordering for higher-order terms. In: Proceedings of the 15th International Conference On Rewriting Techniques and Applications, LNCS 3091 (RTA2004), pp. 40\u201354 (2004)","DOI":"10.1007\/978-3-540-25979-4_3"},{"key":"46_CR38","volume-title":"Elements of ML Programming","author":"Ullman","year":"1997","unstructured":"Ullman, Jeffrey D.: Elements of ML Programming. Prentice Hall, Englewood cliffs (1997)"},{"issue":"4","key":"46_CR39","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF03177743","volume":"32","author":"X. Urbain","year":"2004","unstructured":"Urbain X. (2004). Modular & incremental automated termination proofs. J. Automated Reason. 32(4): 315\u2013355","journal-title":"J. Automated Reason."}],"container-title":["Applicable Algebra in Engineering, Communication and Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-007-0046-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00200-007-0046-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00200-007-0046-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T15:24:20Z","timestamp":1558625060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00200-007-0046-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,11]]},"references-count":39,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,9,25]]}},"alternative-id":["46"],"URL":"https:\/\/doi.org\/10.1007\/s00200-007-0046-9","relation":{},"ISSN":["0938-1279","1432-0622"],"issn-type":[{"value":"0938-1279","type":"print"},{"value":"1432-0622","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7,11]]}}}