{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:03:47Z","timestamp":1773479027843,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["Core- to-Core Program (A. Advanced Research Networks)"],"award-info":[{"award-number":["Core- to-Core Program (A. Advanced Research Networks)"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001700","name":"Ministry of Education, Culture, Sports, Science, and Technology","doi-asserted-by":"publisher","award":["Kakenhi 26330082, 25280023, 15H05706, 23220001, 25730035, and 25280020"],"award-info":[{"award-number":["Kakenhi 26330082, 25280023, 15H05706, 23220001, 25730035, and 25280020"]}],"id":[{"id":"10.13039\/501100001700","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837667","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"57-68","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Temporal verification of higher-order functional programs"],"prefix":"10.1145","author":[{"given":"Akihiro","family":"Murase","sequence":"first","affiliation":[{"name":"Nagoya University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[{"name":"JAIST, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ryosuke","family":"Sato","sequence":"additional","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"University of Tsukuba, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"Lecture Notes in Computer Science","first-page":"17","volume-title":"T. \u00c6","author":"Ben-Amram A. M.","unstructured":"A. M. Ben-Amram . General size-change termination and lexicographic descent . In T. \u00c6 . Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation, Complexity, Analysis , Transformation. Essays Dedicated to Neil D. Jones {on occasion of his 60th birthday}, volume 2566 of Lecture Notes in Computer Science , pages 3\u2013 17 . Springer, 2002. A. M. Ben-Amram. General size-change termination and lexicographic descent. In T. \u00c6. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones {on occasion of his 60th birthday}, volume 2566 of Lecture Notes in Computer Science, pages 3\u201317. Springer, 2002."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926431"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491969"},{"key":"e_1_3_2_1_5_1","series-title":"Lecture Notes in Computer Science","first-page":"348","volume-title":"Computer Aided Verification - 23rd International Conference, CAV","author":"Cook B.","year":"2011","unstructured":"B. Cook , E. Koskinen , and M. Y. Vardi . Temporal property verification as a program analysis task . In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011 , Snowbird, UT , USA, July 14-20, 2011. Proceedings , volume 6806 of Lecture Notes in Computer Science , pages 333\u2013 348 . Springer, 2011. B. Cook, E. Koskinen, and M. Y. Vardi. Temporal property verification as a program analysis task. In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 333\u2013348. Springer, 2011."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_3_2_1_8_1","series-title":"Lecture Notes in Computer Science","first-page":"340","volume-title":"TACAS","author":"de Moura L. M.","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: An efficient SMT solver . In TACAS , volume 4963 of Lecture Notes in Computer Science , pages 337\u2013 340 . Springer, 2008. L. M. de Moura and N. Bj\u00f8rner. Z3: An efficient SMT solver. In TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337\u2013340. Springer, 2008."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890030"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603127"},{"key":"e_1_3_2_1_12_1","volume-title":"B\u00fcchi types for infinite traces and liveness. CoRR, abs\/1401.5107","author":"Hofmann M.","year":"2014","unstructured":"M. Hofmann and W. Chen . B\u00fcchi types for infinite traces and liveness. CoRR, abs\/1401.5107 , 2014 . M. Hofmann and W. Chen. B\u00fcchi types for infinite traces and liveness. CoRR, abs\/1401.5107, 2014."},{"key":"e_1_3_2_1_13_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/978-3-642-18275-4","volume-title":"Computer Aided Verification - 23rd International Conference, CAV","author":"Jhala R.","year":"2011","unstructured":"R. Jhala , R. Majumdar , and A. Rybalchenko . HMC: verifying functional programs using abstract interpreters . In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011 , Snowbird, UT , USA, July 14-20, 2011. Proceedings , volume 6806 of Lecture Notes in Computer Science , pages 470\u2013 485 . Springer, 2011. R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: verifying functional programs using abstract interpreters. In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 470\u2013485. Springer, 2011."},{"key":"e_1_3_2_1_14_1","first-page":"203","volume-title":"FPCA","author":"Johnsson T.","year":"1985","unstructured":"T. Johnsson . Lambda lifting : Treansforming programs to recursive equations . In FPCA , pages 190\u2013 203 , 1985 . T. Johnsson. Lambda lifting: Treansforming programs to recursive equations. In FPCA, pages 190\u2013203, 1985."},{"key":"e_1_3_2_1_15_1","volume-title":"Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science, 4(1)","author":"Jones N. D.","year":"2008","unstructured":"N. D. Jones and N. Bohr . Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science, 4(1) , 2008 . N. D. Jones and N. Bohr. Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science, 4(1), 2008."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_2_1_19_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II","volume":"9207","author":"Kuwahara T.","year":"2015","unstructured":"T. Kuwahara , R. Sato , H. Unno , and N. Kobayashi . Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In D. Kroening and C. S. Pasareanu, editors, Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II , volume 9207 of Lecture Notes in Computer Science, pages 287\u2013303. Springer , 2015 . T. Kuwahara, R. Sato, H. Unno, and N. Kobayashi. Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In D. Kroening and C. S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 287\u2013303. Springer, 2015."},{"key":"e_1_3_2_1_20_1","volume-title":"ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings","volume":"8410","author":"Kuwahara T.","year":"2014","unstructured":"T. Kuwahara , T. Terauchi , H. Unno , and N. Kobayashi . Automatic termination verification for higher-order functional programs. In Z. Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming , ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings , volume 8410 of Lecture Notes in Computer Science, pages 392\u2013411. Springer , 2014 . T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination verification for higher-order functional programs. In Z. Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 392\u2013411. Springer, 2014."},{"key":"e_1_3_2_1_21_1","volume-title":"Model checking liveness properties of higher-order functional programs. URL https:\/\/mjolnir.comlab.ox.ac.uk\/papers\/ thors.pdf","author":"Lester M. M.","year":"2011","unstructured":"M. M. Lester , R. P. Neatherway , C.-H. L. Ong , and S. J. Ramsay . Model checking liveness properties of higher-order functional programs. URL https:\/\/mjolnir.comlab.ox.ac.uk\/papers\/ thors.pdf , 2011 . M. M. Lester, R. P. Neatherway, C.-H. L. Ong, and S. J. Ramsay. Model checking liveness properties of higher-order functional programs. URL https:\/\/mjolnir.comlab.ox.ac.uk\/papers\/ thors.pdf, 2011."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632381"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_9"},{"key":"e_1_3_2_1_25_1","series-title":"Lecture Notes in Computer Science","first-page":"251","volume-title":"VMCAI","author":"Podelski A.","unstructured":"A. Podelski and A. Rybalchenko . A complete method for the synthesis of linear ranking functions . In VMCAI , volume 2937 of Lecture Notes in Computer Science , pages 239\u2013 251 . Springer, 2004. A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, volume 2937 of Lecture Notes in Computer Science, pages 239\u2013251. Springer, 2004."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426900"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006466"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706315"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429081"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_38_1","volume-title":"JAIST RCSV-Logic Workshop, 2014","author":"Yokoyama K.","year":"2014","unstructured":"K. Yokoyama . Ramsey\u2019s theorem and termination analysis . In JAIST RCSV-Logic Workshop, 2014 . http:\/\/www.jaist.ac.jp\/rcsv\/ event\/ 2014 1030-eventws\/yokoyama.pdf. K. Yokoyama. Ramsey\u2019s theorem and termination analysis. In JAIST RCSV-Logic Workshop, 2014. http:\/\/www.jaist.ac.jp\/rcsv\/ event\/20141030-eventws\/yokoyama.pdf."}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837667","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:38Z","timestamp":1750211018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":37,"alternative-id":["10.1145\/2837614.2837667","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837667","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837667","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}