{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T04:51:55Z","timestamp":1648529515076},"reference-count":24,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. &amp; Syst."],"published-print":{"date-parts":[[2018,6,1]]},"DOI":"10.1587\/transinf.2017fop0004","type":"journal-article","created":{"date-parts":[[2018,5,31]],"date-time":"2018-05-31T18:50:18Z","timestamp":1527792618000},"page":"1491-1502","source":"Crossref","is-referenced-by-count":1,"title":["Static Dependency Pair Method in Functional Programs"],"prefix":"10.1587","volume":"E101.D","author":[{"given":"Keiichirou","family":"KUSAKARI","sequence":"first","affiliation":[{"name":"Informatics Course, Department of Electrical, Electronic and Computer Engineering, Faculty of Engineering, Gifu University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"publisher","unstructured":"[1] T. Arts and J. Giesl, \u201cTermination of Term Rewriting Using Dependency Pairs,\u201d Theoretical Computer Science, vol.236, no.1-2, pp.133-178, 2000. 10.1016\/s0304-3975(99)00207-8","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"2","doi-asserted-by":"crossref","unstructured":"[2] K. Bimb\u00f3, Combinatory Logic: Pure, Applied and Typed, Chapman and Hall\/CRC, 2011.","DOI":"10.1201\/b11046"},{"key":"3","doi-asserted-by":"publisher","unstructured":"[3] F. Blanqui, J.-P. Jouannaud, and M. Okada, \u201cInductive-Data-Type Systems,\u201d Theoretical Computer Science, vol.272, no.1-2, pp.41-68, 2002. 10.1016\/s0304-3975(00)00347-9","DOI":"10.1016\/S0304-3975(00)00347-9"},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] F. Blanqui, \u201cComputability Closure: Ten Years Later,\u201d In Essay in Honour of Jean-Pierre Jouannaud&apos;s 60 Birthday, LNCS 4600, pp.68-88, 2007.","DOI":"10.1007\/978-3-540-73147-4_4"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] F. Blanqui, J.-P. Jouannaud, and A. Rubio, \u201cThe Computability Path Ordering: The End of a Quest,\u201d Proc. 17th EACSL Annual Conf. on Computer Science Logic, LNCS 5213 (CSL2008), pp.1-14, 2008.","DOI":"10.1007\/978-3-540-87531-4_1"},{"key":"6","doi-asserted-by":"publisher","unstructured":"[6] N. Dershowitz, \u201cOrderings for Term-Rewriting Systems,\u201d Theoretical Computer Science, vol.17, no.3, pp.279-301, 1982. 10.1016\/0304-3975(82)90026-3","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] J. Giesl, R. Thiemann, P. Schneider-Kamp, and S. Falke, \u201cMechanizing and Improving Dependency Pairs,\u201d Journal of Automated Reasoning, vol.37, no.3, pp.155-203, 2006. 10.1007\/s10817-006-9057-7","DOI":"10.1007\/s10817-006-9057-7"},{"key":"8","unstructured":"[8] J.-Y. Girard, \u201cInterpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l&apos;arithm\u00e9tique d&apos;ordre sup\u00e9rieur,\u201d PhD thesis, University of Paris VII, 1972."},{"key":"9","unstructured":"[9] J.R. Hindley and J.P. Seldin, Introduction to Combinators and <i>\u03bb<\/i>-Calculus, Cambridge Univ. Press, 1986."},{"key":"10","doi-asserted-by":"publisher","unstructured":"[10] N. Hirokawa and A. Middeldorp, \u201cTyrolean Termination Tool: Techniques and Features,\u201d Information and Computation, vol.205, no.4, pp.474-511, 2007. 10.1016\/j.ic.2006.08.010","DOI":"10.1016\/j.ic.2006.08.010"},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] J.-P. Jouannaud and A. Rubio, \u201cPolymorphic Higher-Order Recursive Path Orderings,\u201d JACM, vol.54, no.1, pp.1-48, 2007. 10.1145\/1206035.1206037","DOI":"10.1145\/1206035.1206037"},{"key":"12","doi-asserted-by":"publisher","unstructured":"[12] J.W. Klop, V. van Oostrom, and R. de Vrijer, \u201cLambda Calculus with Patterns,\u201d Theoretical Computer Science, vol.398, no.1-3, pp.16-31, 2008. 10.1016\/j.tcs.2008.01.019","DOI":"10.1016\/j.tcs.2008.01.019"},{"key":"13","unstructured":"[13] C. Kop, \u201cHigher Order Termination,\u201d Ph.D. thesis, Vrije Universiteit Amsterdam, 2012."},{"key":"14","unstructured":"[14] K. Kusakari, \u201cOn Proving Termination of Term Rewriting Systems with Higher-Order Variables,\u201d IPSJ Transactions on Programming, vol.42, no.SIG 7 (PRO 11), pp.35-45, 2001."},{"key":"15","doi-asserted-by":"publisher","unstructured":"[15] K. Kusakari, M. Nakamura, and Y. Toyama, \u201cElimination Transformations for Associative-Commutative Rewriting Systems,\u201d Journal of Automated Reasoning, vol.37, no.3, pp.205-229, 2006. 10.1007\/s10817-006-9053-y","DOI":"10.1007\/s10817-006-9053-y"},{"key":"16","doi-asserted-by":"publisher","unstructured":"[16] K. Kusakari and M. Sakai, \u201cEnhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting,\u201d Applicable Algebra in Engineering, Communication and Computing, vol.18, no.5, pp.407-431, 2007. 10.1007\/s00200-007-0046-9","DOI":"10.1007\/s00200-007-0046-9"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] K. Kusakari and M. Sakai, \u201cStatic Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques,\u201d IEICE Trans. Inf. &amp; Syst., vol.E92-D, no.2, pp.235-247, 2009. 10.1587\/transinf.e92.d.235","DOI":"10.1587\/transinf.E92.D.235"},{"key":"18","doi-asserted-by":"publisher","unstructured":"[18] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui, \u201cStatic Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems,\u201d IEICE Trans. Inf. &amp; Syst., vol.E92-D, no.10, pp.2007-2015, 2009. 10.1587\/transinf.e92.d.2007","DOI":"10.1587\/transinf.E92.D.2007"},{"key":"19","doi-asserted-by":"publisher","unstructured":"[19] K. Kusakari, \u201cStatic Dependency Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types,\u201d IEICE Trans. Inf. &amp; Syst., vol.E96-D, no.3, pp.472-480, 2013. 10.1587\/transinf.e96.d.472","DOI":"10.1587\/transinf.E96.D.472"},{"key":"20","doi-asserted-by":"crossref","unstructured":"[20] T. Nipkow, \u201cHigher-order Critical Pairs,\u201d Proc. 6th Annual IEEE Symposium on Logic in Computer Science, pp.342-349, 1991. 10.1109\/lics.1991.151658","DOI":"10.1109\/LICS.1991.151658"},{"key":"21","unstructured":"[21] T. Sakurai, K. Kusakari, M. Sakai, T. Sakabe, and N. Nishida, \u201cUsable Rules and Labeling Product-Typed Terms for Dependency Pair Method in Simply-Typed Term Rewriting Systems,\u201d IEICE Trans. Inf. &amp; Syst., vol.J90-D, no.4, pp.978-989, 2007. (in Japanese)"},{"key":"22","doi-asserted-by":"crossref","unstructured":"[22] S. Suzuki, K. Kusakari, and F. Blanqui, \u201cArgument Filterings and Usable Rules in Higher-Order Rewrite Systems,\u201d IPSJ Transactions on Programming, vol.4, no.2, pp.1-12, 2011.","DOI":"10.2197\/ipsjtrans.4.114"},{"key":"23","doi-asserted-by":"publisher","unstructured":"[23] W.W. Tait, \u201cIntensional Interpretations of Functionals of Finite Type,\u201d Journal of Symbolic Logic, vol.32, no.2, pp.198-212, 1967. 10.2307\/2271658","DOI":"10.2307\/2271658"},{"key":"24","unstructured":"[24] Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol.55, Cambridge University Press, 2003."}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E101.D\/6\/E101.D_2017FOP0004\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T19:07:45Z","timestamp":1571425665000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E101.D\/6\/E101.D_2017FOP0004\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,1]]},"references-count":24,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2017fop0004","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"value":"0916-8532","type":"print"},{"value":"1745-1361","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,6,1]]}}}