{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:03:46Z","timestamp":1773479026761,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548321","type":"print"},{"value":"9783642548338","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54833-8_21","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:37:17Z","timestamp":1395394637000},"page":"392-411","source":"Crossref","is-referenced-by-count":35,"title":["Automatic Termination Verification for Higher-Order Functional Programs"],"prefix":"10.1007","author":[{"given":"Takuya","family":"Kuwahara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"issue":"2-3","key":"21_CR2","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. Higher-Order and Symbolic Computation\u00a014(2-3), 261\u2013300 (2001)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426. ACM (2006)","DOI":"10.1145\/1133255.1134029"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 47\u201361. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_4"},{"issue":"2","key":"21_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1890028.1890030","volume":"33","author":"J. Giesl","year":"2011","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems\u00a033(2), 7:1\u20137:39 (2011)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with aProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-15769-1_4","volume-title":"Static Analysis","author":"M. Heizmann","year":"2010","unstructured":"Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 22\u201350. Springer, Heidelberg (2010)"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv.\u00a041(4) (2009)","DOI":"10.1145\/1592434.1592438"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-22110-1_38","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2011","unstructured":"Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying functional programs using abstract interpreters. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 470\u2013485. Springer, Heidelberg (2011)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Bohr, N.: Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science\u00a04(1) (2008)","DOI":"10.2168\/LMCS-4(1:3)2008"},{"issue":"2-3","key":"21_CR13","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1023\/A:1012944815270","volume":"14","author":"N. Kobayashi","year":"2001","unstructured":"Kobayashi, N.: Type-based useless-variable elimination. Higher-Order and Symbolic Computation\u00a014(2-3), 221\u2013260 (2001)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Model checking higher-order programs. Journal of the ACM\u00a060(3) (2013)","DOI":"10.1145\/2487241.2487246"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: LICS, pp. 179\u2013188. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.29"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI, pp. 222\u2013233. ACM (2011)","DOI":"10.1145\/1993316.1993525"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs (2013), http:\/\/www-kb.is.s.u-tokyo.ac.jp\/~kuwahara\/termination","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-33125-1_26","volume-title":"Static Analysis","author":"R. Ledesma-Garza","year":"2012","unstructured":"Ledesma-Garza, R., Rybalchenko, A.: Binary reachability analysis of higher order functional programs. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 388\u2013404. Springer, Heidelberg (2012)"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392. ACM (2001)","DOI":"10.1145\/373243.360210"},{"key":"21_CR20","unstructured":"Lester, M.M., Neatherway, R.P., Ong, C.H.L., Ramsay, S.J.: Model checking liveness properties of higher-order functional programs. In: Proceedings of ML Workshop\u00a02011 (2011)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS, pp. 81\u201390. IEEE Computer Society (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011, pp. 587\u2013598. ACM (2011)","DOI":"10.1145\/1925844.1926453"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI, pp. 159\u2013169. ACM (2008)","DOI":"10.1145\/1379022.1375602"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Sereni, D.: Termination analysis of higher-order functional programs. Ph.D. thesis, Magdalen College (2006)","DOI":"10.1007\/11575467_19"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Sereni, D.: Termination analysis and call graph construction for higher-order functional programs. In: ICFP, pp. 71\u201384. ACM (2007)","DOI":"10.1145\/1291220.1291165"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11575467_19","volume-title":"Programming Languages and Systems","author":"D. Sereni","year":"2005","unstructured":"Sereni, D., Jones, N.D.: Termination analysis of higher-order functional programs. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 281\u2013297. Springer, Heidelberg (2005)"},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: POPL, pp. 119\u2013130. ACM (2010)","DOI":"10.1145\/1707801.1706315"},{"issue":"4","key":"21_CR32","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s00200-005-0179-7","volume":"16","author":"R. Thiemann","year":"2005","unstructured":"Thiemann, R., Giesl, J.: The size-change principle and dependency pairs for termination of term rewriting. Appl. Algebra Eng. Commun. Comput.\u00a016(4), 229\u2013270 (2005)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: POPL, pp. 75\u201386. ACM (2013)","DOI":"10.1145\/2480359.2429081"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Wand, M., Siveroni, I.: Constraint systems for useless variable elimination. In: Proceedings of POPL 1999, pp. 291\u2013302 (1999)","DOI":"10.1145\/292540.292567"},{"key":"21_CR35","unstructured":"Xi, H.: Dependent types for program termination verification. In: LICS 2001, pp. 231\u2013242. IEEE (2001)"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL, pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"},{"key":"21_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-35873-9_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H. Zhu","year":"2013","unstructured":"Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 295\u2013314. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54833-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:45:49Z","timestamp":1746157549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54833-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548321","9783642548338"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54833-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}