{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:50:11Z","timestamp":1787068211990,"version":"build-2736575974"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["818616"],"award-info":[{"award-number":["818616"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n                    Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types against properties expressed by formulas of monadic second-order logic. What happens when the program in question, in addition to higher-order functions, also exhibits algebraic effects such as probabilistic choice or global store? The results in the literature range from those, mostly positive, about nondeterministic effects, to those about probabilistic effects, in the presence of which even mere reachability becomes undecidable. This work takes a fresh and general look at the problem, first of all showing that there is an elegant and natural way of viewing higher-order programs producing algebraic effects as ordinary higher-order recursion schemes. We then move on to consider effect handlers, showing that in their presence the model checking problem is bound to be undecidable in the general case, while it stays decidable when handlers have a simple syntactic form, still sufficient to capture so-called\n                    <jats:italic toggle=\"yes\">generic effects<\/jats:italic>\n                    . Along the way, we hint at how a general specification language could look like, this way justifying some of the results in the literature, and deriving new ones.\n                  <\/jats:p>","DOI":"10.1145\/3632929","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"2610-2638","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["On Model-Checking Higher-Order Effectful Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[{"name":"University of Bologna, Bologna, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9767-2011","authenticated-orcid":false,"given":"Alexis","family":"Ghyselen","sequence":"additional","affiliation":[{"name":"University of Bologna, Bologna, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"Andrej Bauer. 2019. What is Algebraic About Algebraic Effects and Handlers? arXiv:1807.05923 [cs.LO]"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.40"},{"key":"e_1_3_1_6_1","first-page":"129","article-title":"Saturation-Based Model Checking of Higher-Order Recursion Schemes","volume":"23","author":"Broadbent Christopher","year":"2013","unstructured":"Christopher Broadbent and Naoki Kobayashi. 2013. Saturation-Based Model Checking of Higher-Order Recursion Schemes. In Proc. of CSL 2013 (LIPIcs, Vol. 23). 129-148.","journal-title":"Proc. of CSL 2013"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.73"},{"key":"e_1_3_1_8_1","first-page":"91","article-title":"B\u00f6hm Trees as Higher-Order Recursive Schemes","volume":"24","author":"Clairambault Pierre","year":"2013","unstructured":"Pierre Clairambault and Andrzej S. Murawski. 2013. B\u00f6hm Trees as Higher-Order Recursive Schemes. In Proc. of FSTTCS 2013 (LIPIcs, Vol. 24). 91-102.","journal-title":"Proc. of FSTTCS 2013"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058022"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke Thomas A. Henzinger Helmut Veith Roderick Bloem et al. 2018. Handbook of model checking. Vol. 10. Springer.","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00049-3"},{"key":"e_1_3_1_12_1","first-page":"1","volume-title":"Proc. of LICS 2017","author":"Dal Lago Ugo","year":"2017","unstructured":"Ugo Dal Lago, Francesco Gavazzo, and Paul Levy. 2017. Effectful applicative bisimilarity: Monads, relators, and Howe\u2019s method. In Proc. of LICS 2017. IEEE, 1-12."},{"key":"e_1_3_1_13_1","doi-asserted-by":"crossref","unstructured":"Ugo Dal Lago and Alexis Ghyselen. 2023. On Model-Checking Higher-Order Effectful Programs (Long Version). arXiv:2308.16542 [cs.LO]","DOI":"10.1145\/3632929"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_3_1_15_1","first-page":"85","volume-title":"Proc. of CAAP 1994","author":"de Groote Philippe","year":"1994","unstructured":"Philippe de Groote. 1994. A CPS-translation of the \u03bb\u03bc-calculus. In Proc. of CAAP 1994. Springer, 85-99."},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","unstructured":"Tim Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proc. of PLDI 1991. ACM 268-277.","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_1_18_1","first-page":"23:1","article-title":"Lifting Sequential Effects to Control Operators","author":"Gordon Colin S.","year":"2020","unstructured":"Colin S. Gordon. 2020. Lifting Sequential Effects to Control Operators. In Proc. of ECOOP 2020 (LIPIcs, Vol. 166). 23:1-23:30.","journal-title":"Proc. of ECOOP 2020 (LIPIcs, Vol. 166)"},{"key":"e_1_3_1_19_1","volume-title":"LNCS","author":"Gr\u00e4del Erich","year":"2003","unstructured":"Erich Gr\u00e4del, Wolfgang Thomas, and Thomas Wilke. 2003. Automata, logics, and infinite games: a guide to current research. LNCS, Vol. 2500. Springer."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.34"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_3_1_22_1","first-page":"18:1","article-title":"Continuation Passing Style for Effect Handlers","author":"Hillerstr\u00f6m Daniel","year":"2017","unstructured":"Daniel Hillerstr\u00f6m, Sam Lindley, Robert Atkey, and K. C. Sivaramakrishnan. 2017. Continuation Passing Style for Effect Handlers. In Proc. of FSCD 2017 (LIPIcs, Vol. 84). 18:1-18:19.","journal-title":"Proc. of FSCD 2017 (LIPIcs, Vol. 84)"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_1_27_1","first-page":"385","volume-title":"Commun.","author":"King James","year":"1976","unstructured":"James King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385-394."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_21"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_15"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_18"},{"issue":"4","key":"e_1_3_1_32_1","article-title":"On the termination problem for probabilistic higher-order recursive programs","volume":"16","author":"Kobayashi Naoki","year":"2020","unstructured":"Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2020. On the termination problem for probabilistic higher-order recursive programs. Logical Methods in Computer Science 16, 4 (2020).","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_24"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706355"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_37_1","volume-title":"Master\u2019s thesis","author":"Matache Cristina","year":"2018","unstructured":"Cristina Matache. 2018. Program equivalence for algebraic effects via modalities.. In Master\u2019s thesis. University of Oxford, Department of Computer Science."},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_22"},{"key":"e_1_3_1_39_1","unstructured":"Eugenio Moggi. 1988. Computational Lambda-calculus and Monads. University of Edinburgh Department of Computer Science."},{"key":"e_1_3_1_40_1","first-page":"21:1","article-title":"On Average-Case Hardness of Higher-Order Model Checking","author":"Nakamura Yoshiki","year":"2020","unstructured":"Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin\u2019ya, and Takeshi Tsukada. 2020. On Average-Case Hardness of Higher-Order Model Checking. In Proc. of FSCD 2020 (LIPIcs, Vol. 167). 21:1-21:23.","journal-title":"Proc. of FSCD 2020 (LIPIcs, Vol. 167)"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364578"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.9"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535873"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33512-9_2"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.012"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426900"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408999"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_1_55_1","first-page":"4:1","article-title":"Behavioural Equivalence via Modalities for Algebraic Effects","author":"Simpson Alex","year":"2019","unstructured":"Alex Simpson and Niels Voorneveld. 2019. Behavioural Equivalence via Modalities for Algebraic Effects. ACM Trans. Program. Lang. Syst. 42 (2019), 4:1-4:45.","journal-title":"ACM Trans. Program. Lang. Syst. 42"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_5"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_12"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287593"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3026744.3026745"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632929","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:05:19Z","timestamp":1751645119000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632929"],"URL":"https:\/\/doi.org\/10.1145\/3632929","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}