{"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":1773479027402,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"JSPS KAKENHI","award":["JP22K17875, JP24H00699, JP20H04162, JP22H03564, JP22H03570, JP20H05703"],"award-info":[{"award-number":["JP22K17875, JP24H00699, JP20H04162, JP22H03564, JP22H03570, JP20H05703"]}]},{"name":"JST CREST","award":["JPMJCR21M3"],"award-info":[{"award-number":["JPMJCR21M3"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>\n                    Since the seminal work by Ong, the model checking of higher-order programs\u2014called\n                    <jats:italic toggle=\"yes\">higher-order model checking<\/jats:italic>\n                    , or HOMC for short\u2014has gained attention. It is also crucial for making HOMC applicable to real-world software to address programs involving computational effects. Recently, Dal Lago and Ghyselen considered an extension of HOMC to\n                    <jats:italic toggle=\"yes\">algebraic effect handlers<\/jats:italic>\n                    , which enable programming the semantics of effects. They showed a negative result for HOMC with algebraic effect handlers\u2014it is undecidable. In this work, we explore a restriction on programs with algebraic effect handlers which ensures the decidability of HOMC while allowing implementations of various effects. We identify the crux of the undecidability as the use of an unbounded number of algebraic effect handlers being active at the same time. To prevent it, we introduce\n                    <jats:italic toggle=\"yes\">answer-type modification<\/jats:italic>\n                    (ATM), which can bound the number of algebraic effect handlers that can be active at the same time. We prove that ATM can ensure the decidability of HOMC and show that it accommodates a wide range of effects. To evaluate our approach, we implemented an automated verifier EffCaml based on the presented techniques and confirmed that the program examples discussed in this paper can be automatically verified.\n                  <\/jats:p>","DOI":"10.1145\/3689805","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2662-2691","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"},{"name":"SOKENDAI, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_2_2_1","volume-title":"Principles of model checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_4_1","unstructured":"Christopher H. Broadbent and Naoki Kobayashi. 2013. Saturation-Based Model Checking of Higher-Order Recursion Schemes. In Computer Science Logic 2013 (CSL 2013) CSL 2013 September 2-5 2013 Torino Italy (LIPIcs Vol. 23) Simona Ronchi Della Rocca (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 129\u2013148. https:\/\/doi.org\/10.4230\/LIPICS.CSL.2013.129 10.4230\/LIPICS.CSL.2013.129"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113767"},{"key":"e_1_3_2_6_1","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke Thomas A. Henzinger Helmut Veith and Roderick Bloem (Eds.). 2018. Handbook of Model Checking. Springer. https:\/\/doi.org\/10.1007\/978-3-319-10575-8 10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21314-4_4"},{"key":"e_1_3_2_8_1","unstructured":"Youyou Cong Chiaki Ishio Kaho Honda and Kenichi Asai. 2021. A Functional Abstraction of Typed Invocation Contexts. In 6th International Conference on Formal Structures for Computation and Deduction FSCD 2021 July 17-24 2021 Buenos Aires Argentina (Virtual Conference) (LIPIcs Vol. 195) Naoki Kobayashi (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 12:1\u201312:18. https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2021.12 10.4230\/LIPICS.FSCD.2021.12"},{"key":"e_1_3_2_9_1","unstructured":"Ugo Dal Lago. 2024. Private communication."},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632929"},{"key":"e_1_3_2_11_1","doi-asserted-by":"crossref","unstructured":"Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In LISP and Functional Programming. 151\u2013160. https:\/\/doi.org\/10.1145\/91556.91622 10.1145\/91556.91622","DOI":"10.1145\/91556.91622"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434314"},{"key":"e_1_3_2_13_1","first-page":"13:1","article-title":"On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control","volume":"1","author":"Forster Yannick","year":"2017","unstructured":"Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. 2017. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. PACMPL 1, ICFP (2017), 13:1\u201313:29. https:\/\/doi.org\/10.1145\/3110257 10.1145\/3110257","journal-title":"PACMPL"},{"key":"e_1_3_2_14_1","first-page":"23:1","volume-title":"34th European Conference on Object-Oriented Programming, ECOOP 2020 (LIPIcs, Vol. 166)","author":"Gordon. Colin S.","year":"2020","unstructured":"Colin S. Gordon. 2020. Lifting Sequential Effects to Control Operators. In 34th European Conference on Object-Oriented Programming, ECOOP 2020 (LIPIcs, Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 23:1\u201323:30. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.23 10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.34"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3564719.3568691"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_3_2_18_1","doi-asserted-by":"crossref","unstructured":"Yukiyoshi Kameyama and Takuo Yonezawa. 2008. Typed Dynamic Control Operators for Delimited Continuations. In Functional and Logic Programming 9th International Symposium FLOPS 2008. 239\u2013254. https:\/\/doi.org\/10.1007\/978-3-540-78969-7_18 10.1007\/978-3-540-78969-7_18","DOI":"10.1007\/978-3-540-78969-7_18"},{"key":"e_1_3_2_19_1","doi-asserted-by":"crossref","unstructured":"Ohad Kammar Sam Lindley and Nicolas Oury. 2013. Handlers in action. In ACM SIGPLAN International Conference on Functional Programming ICFP 2013. 145\u2013158. https:\/\/doi.org\/10.1145\/2500365.2500590 10.1145\/2500365.2500590","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3633280"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632898"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_3_2_24_1","unstructured":"Naoki Kobayashi. 2016. HorSat2: A Saturation-Based Model Checker for Higher-Order Recursion Schemes. Private communication. Available at https:\/\/github.com\/hopv\/horsat2.."},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785679"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_24"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009854"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706355"},{"key":"e_1_3_2_32_1","doi-asserted-by":"crossref","unstructured":"Sam Lindley. 2014. Algebraic effects and effect handlers for idioms and arrows. In Proceedings of the 10th ACM SIGPLAN workshop on Generic programming WGP 2014 Gothenburg Sweden August 31 2014 Jos\u00e9 Pedro Magalh\u00e3es and Tiark Rompf (Eds.). ACM 47\u201358. https:\/\/doi.org\/10.1145\/2633628.2633636 10.1145\/2633628.2633636","DOI":"10.1145\/2633628.2633636"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000212"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_22"},{"key":"e_1_3_2_35_1","doi-asserted-by":"crossref","unstructured":"Marek Materzok and Dariusz Biernacki. 2011. Subtyping Delimited Continuations. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming ICFP 2011 Manuel M. T. Chakravarty Zhenjiang Hu and Olivier Danvy (Eds.). ACM 81\u201393. https:\/\/doi.org\/10.1145\/2034773.2034786 10.1145\/2034773.2034786","DOI":"10.1145\/2034773.2034786"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_16"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_38_1","doi-asserted-by":"crossref","unstructured":"C.-H. Luke Ong and Steven J. Ramsay. 2011. Verifying higher-order functional programs with pattern-matching algebraic data types. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2011 Austin TX USA January 26-28 2011 Thomas Ball and Mooly Sagiv (Eds.). ACM 587\u2013598. https:\/\/doi.org\/10.1145\/1926385.1926453 10.1145\/1926385.1926453","DOI":"10.1145\/1926385.1926453"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_3_2_43_1","doi-asserted-by":"crossref","unstructured":"Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In Programming Languages and Systems 18th European Symposium on Programming ESOP 2009 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2009 Proceedings. 80\u201394. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_7 10.1007\/978-3-642-00590-9_7","DOI":"10.1007\/978-3-642-00590-9_7"},{"issue":"4","key":"e_1_3_2_44_1","article-title":"Handling Algebraic Effects","volume":"9","author":"Plotkin Gordon D.","year":"2013","unstructured":"Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Logical Methods in Computer Science 9, 4 (2013). https:\/\/doi.org\/10.2168\/LMCS-9(4:23)2013 10.2168\/LMCS-9(4:23)2013","journal-title":"Logical Methods in Computer Science"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_3_2_47_1","doi-asserted-by":"crossref","unstructured":"Steven J. Ramsay Robin P. Neatherway and C.-H. Luke Ong. 2014. A type-directed abstraction refinement approach to higher-order model checking. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL\u201914 San Diego CA USA January 20-21 2014 Suresh Jagannathan and Peter Sewell (Eds.). ACM 61\u201372. https:\/\/doi.org\/10.1145\/2535838.2535873 10.1145\/2535838.2535873","DOI":"10.1145\/2535838.2535873"},{"key":"e_1_3_2_48_1","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In Proceedings of the ACM Annual Conference - Volume 2 (ACM\u201972). 717\u2013740. https:\/\/doi.org\/10.1145\/800194.805852 10.1145\/800194.805852","DOI":"10.1145\/800194.805852"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.012"},{"key":"e_1_3_2_50_1","doi-asserted-by":"crossref","unstructured":"Ryosuke Sato Hiroshi Unno and Naoki Kobayashi. 2013. Towards a scalable software model checker for higher-order programs. In Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation PEPM 2013 Elvira Albert and Shin-Cheng Mu (Eds.). ACM 53\u201362. https:\/\/doi.org\/10.1145\/2426890.2426900 10.1145\/2426890.2426900","DOI":"10.1145\/2426890.2426900"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408975"},{"key":"e_1_3_2_52_1","doi-asserted-by":"crossref","unstructured":"Taro Sekiyama and Hiroshi Unno. 2023. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. Proc. ACM Program. Lang. 7 POPL Article 71 (2023) 32 pages. https:\/\/doi.org\/10.1145\/3571264 10.1145\/3571264","DOI":"10.1145\/3571264"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_5"},{"key":"e_1_3_2_54_1","doi-asserted-by":"crossref","unstructured":"Nikhil Swamy Joel Weinberger Cole Schlesinger Juan Chen and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. In ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI\u201913 Seattle WA USA June 16-19 2013 Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM 387\u2013398. https:\/\/doi.org\/10.1145\/2491956.2491978 10.1145\/2491956.2491978","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_55_1","first-page":"343","volume-title":"Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6014)","author":"Tsukada Takeshi","year":"2010","unstructured":"Takeshi Tsukada and Naoki Kobayashi. 2010. Untyped Recursion Schemes and Infinite Intersection Types. In Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6014), C.-H. Luke Ong (Ed.). Springer, 343\u2013357. https:\/\/doi.org\/10.1007\/978-3-642-12032-9_24 10.1007\/978-3-642-12032-9_24"},{"key":"e_1_3_2_56_1","first-page":"312","volume-title":"Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6461)","author":"Unno Hiroshi","year":"2010","unstructured":"Hiroshi Unno, Naoshi Tabuchi, and Naoki Kobayashi. 2010. Verification of Tree-Processing Programs via Higher-Order Model Checking. In Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6461), Kazunori Ueda (Ed.). Springer, 312\u2013327. https:\/\/doi.org\/10.1007\/978-3-642-17164-2_22 10.1007\/978-3-642-17164-2_22"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689805","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689805","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:04:32Z","timestamp":1770195872000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689805"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":55,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689805"],"URL":"https:\/\/doi.org\/10.1145\/3689805","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}