{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T14:39:41Z","timestamp":1780065581072,"version":"3.54.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319898834","type":"print"},{"value":"9783319898841","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89884-1_25","type":"book-chapter","created":{"date-parts":[[2018,4,14]],"date-time":"2018-04-14T01:02:32Z","timestamp":1523667752000},"page":"711-738","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Higher-Order Program Verification via HFL Model Checking"],"prefix":"10.1007","author":[{"given":"Naoki","family":"Kobayashi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Keiichi","family":"Watanabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-3(2:7)2007","volume":"3","author":"R Axelsson","year":"2007","unstructured":"Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Logical Methods Comput. Sci. 3(2), 1\u201333 (2007)","journal-title":"Logical Methods Comput. Sci."},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: SMT 2012, EPiC Series in Computing, vol. 20, pp. 3\u201311. EasyChair (2012)","DOI":"10.29007\/1l7f"},{"key":"25_CR4","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: Higher-order program verification as satisfiability modulo theories with algebraic data-types. CoRR, abs\/1306.5264 (2013)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-18170-9_151","volume-title":"Computation Theory and Logic","author":"A Blass","year":"1987","unstructured":"Blass, A., Gurevich, Y.: Existential fixed-point logic. In: B\u00f6rger, E. (ed.) Computation Theory and Logic. LNCS, vol. 270, pp. 20\u201336. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-18170-9_151"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-540-89330-1_20","volume-title":"Programming Languages and Systems","author":"M Blume","year":"2008","unstructured":"Blume, M., Acar, U.A., Chae, W.: Exception handlers as extensible cases. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 273\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89330-1_20"},{"issue":"POPL","key":"25_CR7","first-page":"11:1","volume":"2","author":"TC Burn","year":"2018","unstructured":"Burn, T.C., Ong, C.L., Ramsay, S.J.: Higher-order constrained horn clauses for verification. PACMPL 2(POPL), 11:1\u201311:28 (2018)","journal-title":"PACMPL"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Carayol, A., Serre, O.: Collapsible pushdown automata and labeled recursion schemes: equivalence, safety and effective selection. In: LICS 2012, pp. 165\u2013174. IEEE (2012)","DOI":"10.1109\/LICS.2012.73"},{"issue":"8","key":"25_CR9","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games: A Guide to Current Research","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Grellois, C., Melli\u00e8s, P.: Relational semantics of linear logic and higher-order model checking. In: Proceedings of CSL 2015, LIPIcs, vol. 41, pp. 260\u2013276 (2015)","DOI":"10.1007\/978-3-662-48057-1_20"},{"key":"25_CR12","unstructured":"Haddad, A.: Model checking and functional program transformations. In: Proceedings of FSTTCS 2013, LIPIcs, vol. 24, pp. 115\u2013126 (2013)"},{"issue":"4","key":"25_CR13","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00276020","volume":"26","author":"WH Hesselink","year":"1989","unstructured":"Hesselink, W.H.: Predicate-transformer semantics of general recursion. Acta Inf. 26(4), 309\u2013332 (1989)","journal-title":"Acta Inf."},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Chen, W.: Abstract interpretation from B\u00fcchi automata. In: Proceedings of CSL-LICS 2014, pp. 51:1\u201351:10. ACM (2014)","DOI":"10.1145\/2603088.2603127"},{"issue":"2","key":"25_CR15","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/1057387.1057390","volume":"27","author":"A Igarashi","year":"2005","unstructured":"Igarashi, A., Kobayashi, N.: Resource usage analysis. ACM Trans. Prog. Lang. Syst. 27(2), 264\u2013313 (2005)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/3-540-45931-6_15","volume-title":"Foundations of Software Science and Computation Structures","author":"T Knapik","year":"2002","unstructured":"Knapik, T., Niwi\u0144ski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 205\u2013222. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45931-6_15"},{"issue":"1","key":"25_CR17","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/1594834.1480933","volume":"44","author":"Naoki Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proceedings of POPL, pp. 416\u2013428. ACM Press (2009)","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"25_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2487241.2487246","volume":"60","author":"N Kobayashi","year":"2013","unstructured":"Kobayashi, N.: Model checking higher-order programs. J. ACM 60(3), 1\u201362 (2013)","journal-title":"J. ACM"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Lozes, \u00c9., Bruse, F.: On the relationship between higher-order recursion schemes and higher-order fixpoint logic. In: Proceedings of POPL 2017, pp. 246\u2013259 (2017)","DOI":"10.1145\/3009837.3009854"},{"issue":"1","key":"25_CR20","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s10990-013-9093-z","volume":"25","author":"N Kobayashi","year":"2013","unstructured":"Kobayashi, N., Matsuda, K., Shinohara, A., Yaguchi, K.: Functional programs as compressed data. High.-Order Symbolic Comput. 25(1), 39\u201384 (2013)","journal-title":"High.-Order Symbolic Comput."},{"key":"25_CR21","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: Proceedings of LICS 2009, pp. 179\u2013188 (2009)","DOI":"10.1109\/LICS.2009.29"},{"issue":"6","key":"25_CR22","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1145\/1993316.1993525","volume":"46","author":"Naoki Kobayashi","year":"2011","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of PLDI, pp. 222\u2013233. ACM Press (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"25_CR23","unstructured":"Kobayashi, N., Tsukada, T., Watanabe, K.: Higher-order program verification via HFL model checking. CoRR abs\/1710.08614 (2017). http:\/\/arxiv.org\/abs\/1710.08614"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Koskinen, E., Terauchi, T.: Local temporal reasoning. In: Proceedings of CSL-LICS 2014, pp. 59:1\u201359:10. ACM (2014)","DOI":"10.1145\/2603088.2603138"},{"key":"25_CR25","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$\u03bc-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-21668-3_17","volume-title":"Computer Aided Verification","author":"T Kuwahara","year":"2015","unstructured":"Kuwahara, T., Sato, R., Unno, H., Kobayashi, N.: Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 287\u2013303. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_17"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-54833-8_21","volume-title":"Programming Languages and Systems","author":"T Kuwahara","year":"2014","unstructured":"Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 392\u2013411. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_21"},{"key":"25_CR28","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1016\/j.tcs.2014.08.020","volume":"560","author":"M Lange","year":"2014","unstructured":"Lange, M., Lozes, \u00c9., Guzm\u00e1n, M.V.: Model-checking process equivalences. Theor. Comput. Sci. 560, 326\u2013347 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR29","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. 7460, pp. 388\u2013404. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33125-1_26"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Lozes, \u00c9.: A type-directed negation elimination. In: Proceedings FICS 2015, EPTCS, vol. 191, pp. 132\u2013142 (2015)","DOI":"10.4204\/EPTCS.191.12"},{"issue":"1","key":"25_CR31","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/2914770.2837667","volume":"51","author":"Akihiro Murase","year":"2016","unstructured":"Murase, A., Terauchi, T., Kobayashi, N., Sato, R., Unno, H.: Temporal verification of higher-order functional programs. In: Proceedings of POPL 2016, pp. 57\u201368 (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"25_CR32","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81\u201390. IEEE Computer Society Press (2006)","DOI":"10.1109\/LICS.2006.38"},{"key":"25_CR33","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, pp. 587\u2013598. ACM Press (2011)","DOI":"10.1145\/1926385.1926453"},{"key":"25_CR34","first-page":"159","volume":"2008","author":"PM Rondon","year":"2008","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. PLDI 2008, 159\u2013169 (2008)","journal-title":"PLDI"},{"issue":"2","key":"25_CR35","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1017\/S0956796807006466","volume":"18","author":"C Skalka","year":"2008","unstructured":"Skalka, C., Smith, S.F., Horn, D.V.: Types and trace effects of higher order programs. J. Funct. Program. 18(2), 179\u2013249 (2008)","journal-title":"J. Funct. Program."},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Dependent types from counterexamples. In: Proceedings of POPL, pp. 119\u2013130. ACM (2010)","DOI":"10.1145\/1706299.1706315"},{"key":"25_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-29822-6_22","volume-title":"Functional and Logic Programming","author":"Y Tobita","year":"2012","unstructured":"Tobita, Y., Tsukada, T., Kobayashi, N.: Exact flow analysis by higher-order model checking. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 275\u2013289. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29822-6_22"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Tsukada, T., Ong, C.L.: Compositional higher-order model checking via $$\\omega $$\u03c9-regular games over B\u00f6hm trees. In: Proceedings of CSL-LICS 2014, pp. 78:1\u201378:10. ACM (2014)","DOI":"10.1145\/2603088.2603133"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: PPDP 2009, pp. 277\u2013288. ACM (2009)","DOI":"10.1145\/1599410.1599445"},{"issue":"POPL","key":"25_CR40","first-page":"12:01","volume":"2","author":"H Unno","year":"2018","unstructured":"Unno, H., Satake, Y., Terauchi, T.: Relatively complete refinement type system for verification of higher-order non-deterministic programs. PACMPL 2(POPL), 12:01\u201312:29 (2018)","journal-title":"PACMPL"},{"key":"25_CR41","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: POPL 2013. pp. 75\u201386. ACM (2013)","DOI":"10.1145\/2429069.2429081"},{"key":"25_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-28644-8_33","volume-title":"CONCUR 2004 - Concurrency Theory","author":"M Viswanathan","year":"2004","unstructured":"Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 512\u2013528. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_33"},{"key":"25_CR43","doi-asserted-by":"crossref","unstructured":"Watanabe, K., Sato, R., Tsukada, T., Kobayashi, N.: Automatically disproving fair termination of higher-order functional programs. In: Proceedings of ICFP 2016, pp. 243\u2013255. ACM (2016)","DOI":"10.1145\/2951913.2951919"},{"issue":"9","key":"25_CR44","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1145\/2858949.2784766","volume":"50","author":"He Zhu","year":"2015","unstructured":"Zhu, H., Nori, A.V., Jagannathan, S.: Learning refinement types. In: Proceedings of ICFP 2015, pp. 400\u2013411. ACM (2015)","journal-title":"ACM SIGPLAN Notices"}],"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-319-89884-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,3]],"date-time":"2025-07-03T17:35:33Z","timestamp":1751564133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89884-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319898834","9783319898841"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89884-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}