{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:31:43Z","timestamp":1750221103716,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"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":["JP15H05706,JP16K16004"],"award-info":[{"award-number":["JP15H05706,JP16K16004"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,1,14]]},"DOI":"10.1145\/3294032.3294077","type":"proceedings-article","created":{"date-parts":[[2018,12,20]],"date-time":"2018-12-20T13:41:47Z","timestamp":1545313307000},"page":"22-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Reduction from branching-time property verification of higher-order programs to HFL validity checking"],"prefix":"10.1145","author":[{"given":"Keiichi","family":"Watanabe","sequence":"first","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":"Hiroki","family":"Oshikawa","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":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_2_1","volume-title":"Proceedings of SAIG 2000 (LNCS)","volume":"1924","author":"Berardi Stefano","year":"2000","unstructured":"Stefano Berardi , Mario Coppo , Ferruccio Damiani , and Paola Giannini . 2000 . Type-Based Useless-Code Elimination for Functional Programs . In Proceedings of SAIG 2000 (LNCS) , Vol. 1924 . Springer, 172\u2013189. Stefano Berardi, Mario Coppo, Ferruccio Damiani, and Paola Giannini. 2000. Type-Based Useless-Code Elimination for Functional Programs. In Proceedings of SAIG 2000 (LNCS), Vol. 1924. Springer, 172\u2013189."},{"volume-title":"Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science)","author":"Bj\u00f8rner Nikolaj","key":"e_1_3_2_1_3_1","unstructured":"Nikolaj Bj\u00f8rner , Arie Gurfinkel , Kenneth L. McMillan , and Andrey Rybalchenko . 2015. Horn Clause Solvers for Program Verification . In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science) , Vol. 9300 . Springer , 24\u201351. Nikolaj Bj\u00f8rner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science), Vol. 9300. Springer, 24\u201351."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_22"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863590"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_30"},{"key":"e_1_3_2_1_8_1","volume-title":"CAV","author":"Cook Byron","year":"2015","unstructured":"Byron Cook , Heidy Khlaaf , and Nir Piterman . 2015 . On Automation of CTL* Verification for Infinite-State Systems. In Computer Aided Verification - 27th International Conference , CAV 2015. 13\u201329. Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015. On Automation of CTL* Verification for Infinite-State Systems. In Computer Aided Verification - 27th International Conference, CAV 2015. 13\u201329."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3060257"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491969"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_2"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/938135"},{"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","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704852"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012944815270"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009854"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_1_22_1","volume-title":"Programming Languages and Systems - 27th European Symposium on Programming, ESOP","author":"Kobayashi Naoki","year":"2018","unstructured":"Naoki Kobayashi , Takeshi Tsukada , and Keiichi Watanabe . 2018. Higher-Order Program Verification via HFL Model Checking . In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018 , Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science), Amal Ahmed (Ed.), Vol. 10801 . Springer , 711\u2013738. Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. 2018. Higher-Order Program Verification via HFL Model Checking. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science), Amal Ahmed (Ed.), Vol. 10801. Springer, 711\u2013738."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_17"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of ML Workshop","author":"Lester M. M.","year":"2011","unstructured":"M. M. Lester , R. P. Neatherway , C.-H. Luke Ong , and S. J. Ramsay . 2011. Model checking liveness properties of higher-order functional programs . In Proceedings of ML Workshop 2011 . M. M. Lester, R. P. Neatherway, C.-H. Luke Ong, and S. J. Ramsay. 2011. Model checking liveness properties of higher-order functional programs. In Proceedings of ML Workshop 2011."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceeding of the 24th EACSL Annual Conference on Computer Science Logic, CSL 2015. 229\u2013243","author":"Salvati Sylvain","year":"2015","unstructured":"Sylvain Salvati and Igor Walukiewicz . 2015 . A Model for Behavioural Properties of Higher-order Programs . In Proceeding of the 24th EACSL Annual Conference on Computer Science Logic, CSL 2015. 229\u2013243 . Sylvain Salvati and Igor Walukiewicz. 2015. A Model for Behavioural Properties of Higher-order Programs. In Proceeding of the 24th EACSL Annual Conference on Computer Science Logic, CSL 2015. 229\u2013243."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_3_2_1_32_1","volume-title":"CONCUR (Lecture Notes in Computer Science)","volume":"3170","author":"Viswanathan M.","unstructured":"M. Viswanathan and R. Viswanathan . 2004. A Higher Order Modal Fixed Point Logic . In CONCUR (Lecture Notes in Computer Science) , Vol. 3170 . Springer, 512\u2013528. M. Viswanathan and R. Viswanathan. 2004. A Higher Order Modal Fixed Point Logic. In CONCUR (Lecture Notes in Computer Science), Vol. 3170. Springer, 512\u2013528."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292567"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951919"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Keiichi Watanabe Takeshi Tsukada Hiroki Oshikawa and Naoki Kobayashi. 2019. Reduction from Branching-time Property Verification of Higher-Order Programs to HFL Validity Checking. A longer vesion available at http:\/\/www-kb.is.s.u-tokyo.ac.jp\/~koba\/papers\/pepm2019-full.pdf .  Keiichi Watanabe Takeshi Tsukada Hiroki Oshikawa and Naoki Kobayashi. 2019. Reduction from Branching-time Property Verification of Higher-Order Programs to HFL Validity Checking. A longer vesion available at http:\/\/www-kb.is.s.u-tokyo.ac.jp\/~koba\/papers\/pepm2019-full.pdf .","DOI":"10.1145\/3294032.3294077"}],"event":{"name":"POPL '19: 46th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"Cascais Portugal","acronym":"POPL '19"},"container-title":["Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3294032.3294077","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3294032.3294077","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:01:47Z","timestamp":1750208507000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3294032.3294077"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":35,"alternative-id":["10.1145\/3294032.3294077","10.1145\/3294032"],"URL":"https:\/\/doi.org\/10.1145\/3294032.3294077","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}