{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:59Z","timestamp":1772164019246,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,9,4]],"date-time":"2016-09-04T00:00:00Z","timestamp":1472947200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,9,4]]},"DOI":"10.1145\/2951913.2951919","type":"proceedings-article","created":{"date-parts":[[2016,8,29]],"date-time":"2016-08-29T08:17:16Z","timestamp":1472458636000},"page":"243-255","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Automatically disproving fair termination of higher-order functional programs"],"prefix":"10.1145","author":[{"given":"Keiichi","family":"Watanabe","sequence":"first","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":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,9,4]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3)","author":"Aehlig K.","year":"2007","unstructured":"K. Aehlig . A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3) , 2007 . K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.73"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_2_1_5_1","volume-title":"CAV 2015, Proceedings, Part I","volume":"9206","author":"Cook B.","year":"2015","unstructured":"B. Cook , H. Khlaaf , and N. Piterman . On automation of CTL* verification for infinite-state systems. In Computer Aided Verification - 27th International Conference , CAV 2015, Proceedings, Part I , volume 9206 of Lecture Notes in Computer Science, pages 13\u201329. Springer , 2015 . B. Cook, H. Khlaaf, and N. Piterman. On automation of CTL* verification for infinite-state systems. In Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 13\u201329. Springer, 2015."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_30"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773202"},{"key":"e_1_3_2_1_8_1","volume-title":"14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings","volume":"4963","author":"de Moura L. M.","year":"2008","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems , 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings , volume 4963 of Lecture Notes in Computer Science, pages 337\u2013340. Springer , 2008 . L. M. de Moura and N. Bj\u00f8rner. Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337\u2013340. Springer, 2008."},{"key":"e_1_3_2_1_9_1","volume-title":"HorSatP: A saturation-based higher-order model checker for APT","author":"Fujima K.","year":"2015","unstructured":"K. Fujima . HorSatP: A saturation-based higher-order model checker for APT , 2015 . Tool available from the author. K. Fujima. HorSatP: A saturation-based higher-order model checker for APT, 2015. Tool available from the author."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_2"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890030"},{"key":"e_1_3_2_1_12_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research","author":"Gr\u00e4del E.","year":"2002","unstructured":"E. Gr\u00e4del , W. Thomas , and T. Wilke . Automata, Logics, and Infinite Games: A Guide to Current Research , volume 2500 of Lecture Notes in Computer Science . Springer , 2002 . E. Gr\u00e4del, W. Thomas, and T. Wilke. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002."},{"key":"e_1_3_2_1_13_1","first-page":"126","volume-title":"IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS","volume":"24","author":"Haddad A.","year":"2013","unstructured":"A. Haddad . Model checking and functional program transformations . In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013 , volume 24 of LIPIcs, pages 115\u2013 126 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. A. Haddad. Model checking and functional program transformations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, volume 24 of LIPIcs, pages 115\u2013126. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603127"},{"key":"e_1_3_2_1_15_1","volume-title":"CAV 2011, Proceedings","volume":"6806","author":"Jhala R.","year":"2011","unstructured":"R. Jhala , R. Majumdar , and A. Rybalchenko . HMC: verifying functional programs using abstract interpreters. In Computer Aided Verification - 23rd International Conference , CAV 2011, Proceedings , volume 6806 of Lecture Notes in Computer Science, pages 470\u2013485. Springer , 2011 . R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: verifying functional programs using abstract interpreters. In Computer Aided Verification - 23rd International Conference, CAV 2011, Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 470\u2013485. Springer, 2011."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628159"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"e_1_3_2_1_22_1","volume-title":"CAV 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 Computer Aided Verification - 27th International Conference , CAV 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 Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 287\u2013303. Springer, 2015."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of ML Workshop 2011","author":"Lester M.","year":"2011","unstructured":"M. Lester , R. P. Neatherway , C. L. Ong , and S. J. Ramsay . Model checking liveness properties of higher-order functional programs . In Proceedings of ML Workshop 2011 , 2011 . M. Lester, R. P. Neatherway, C. L. Ong, and S. J. Ramsay. Model checking liveness properties of higher-order functional programs. In Proceedings of ML Workshop 2011, 2011."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632381"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737971"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926453"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"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\/2603088.2603133"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429081"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784766"}],"event":{"name":"ICFP'16: ACM SIGPLAN International Conference on Functional Programming","location":"Nara Japan","acronym":"ICFP'16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951919","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2951913.2951919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:39:36Z","timestamp":1750203576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,4]]},"references-count":36,"alternative-id":["10.1145\/2951913.2951919","10.1145\/2951913"],"URL":"https:\/\/doi.org\/10.1145\/2951913.2951919","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3022670.2951919","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,9,4]]},"assertion":[{"value":"2016-09-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}