{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:45:42Z","timestamp":1787064342853,"version":"build-2736575974"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/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":["JP20H04162, JP20H05703, JP22H03564, JP22H03570, JP24H00699, JP25H00446"],"award-info":[{"award-number":["JP20H04162, JP20H05703, JP22H03564, JP22H03570, JP24H00699, JP25H00446"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"publisher","award":["JPMJCR21M3"],"award-info":[{"award-number":["JPMJCR21M3"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-24-CE48-5521-01"],"award-info":[{"award-number":["ANR-24-CE48-5521-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    Applying higher-order model checking techniques to programs that use effect handlers is a major challenge, given the recent undecidability result obtained by Dal Lago and Ghyselen. This challenge has been addressed by using answer-type modifications, the use of a monomorphic version of which allows to recover decidability. However, the absence of polymorphism leads to a loss of modularity, reusability, and even expressivity. In this work, we study the problem of defining a calculus that on the one hand supports answer-type polymorphism and subtyping but on the other hand ensures the underlying model checking problem to remain decidable. The solution proposed in this paper is based on the introduction of the polymorphic answer-type \u25a1 whose role is to provide a good compromise between expressiveness and decidability, the latter demonstrated through the construction of a selective type-directed CPS transformation targeting a calculus\n                    <jats:italic toggle=\"yes\">without<\/jats:italic>\n                    effect handlers and any form of polymorphism. Noticeably, the introduced calculus\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:msubsup>\n                            <mml:mrow>\n                              <mml:mtext>HEPCF<\/mml:mtext>\n                            <\/mml:mrow>\n                            <mml:mo>\u25a1<\/mml:mo>\n                            <mml:mrow>\n                              <mml:mtext>ATM<\/mml:mtext>\n                            <\/mml:mrow>\n                          <\/mml:msubsup>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    allows the answer types of effects implemented by tail-resumptive effect handlers to be polymorphic. We also implemented a proof-of-concept model checker for\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:msubsup>\n                            <mml:mrow>\n                              <mml:mtext>HEPCF<\/mml:mtext>\n                            <\/mml:mrow>\n                            <mml:mo>\u25a1<\/mml:mo>\n                            <mml:mrow>\n                              <mml:mtext>ATM<\/mml:mtext>\n                            <\/mml:mrow>\n                          <\/mml:msubsup>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    programs.\n                  <\/jats:p>","DOI":"10.1145\/3763184","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"3726-3754","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs"],"prefix":"10.1145","volume":"9","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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Bologna, Italy"},{"name":"INRIA, Sophia Antipolis, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Kenichi Asai and Yukiyoshi Kameyama. 2007. Polymorphic Delimited Continuations. In Programming Languages and Systems 5th Asian Symposium APLAS 2007 Proceedings. 239\u2013254. doi:10.1007\/978-3-540-76637-7_16","DOI":"10.1007\/978-3-540-76637-7_16"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3162069"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276481"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2013.129"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0025774"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69149-5_27"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21314-4_4"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632929"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In LISP and Functional Programming. 151\u2013160. doi:10.1145\/91556.91622","DOI":"10.1145\/91556.91622"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434314"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563445"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.13"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Daniel Hillerstr\u00f6m Sam Lindley Robert Atkey and K. C. Sivaramakrishnan. 2017. Continuation Passing Style for Effect Handlers. In 2nd International Conference on Formal Structures for Computation and Deduction FSCD 2017. 18:1\u201318:19. doi:10.4230\/LIPIcs.FSCD.2017.18","DOI":"10.4230\/LIPIcs.FSCD.2017.18"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Ohad Kammar Sam Lindley and Nicolas Oury. 2013. Handlers in action. In ACM SIGPLAN International Conference on Functional Programming ICFP 2013. 145\u2013158. doi:10.1145\/2500365.2500590","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3633280"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_21"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_15"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599415"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487246"},{"key":"e_1_3_2_31_2","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_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704875"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785679"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706355"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","unstructured":"Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2017. 486\u2013499. http:\/\/dl.acm.org\/citation.cfm?id=3009872","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_2_37_2","volume-title":"Ph. D. Dissertation","author":"Levy Paul Blain","year":"2001","unstructured":"Paul Blain Levy. 2001. Call-by-push-value. Ph. D. Dissertation. Queen Mary University of London, UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.369233"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010020917337"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034786"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201989) Pacific Grove California USA June 5-8 1989. 14\u201323. doi:10.1109\/LICS.1989.39155","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80969-1"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622814"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2004.08.008"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","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. doi:10.1007\/978-3-642-00590-9_7","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2015.12.003"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48523-6_60"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426900"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Taro Sekiyama Ugo Dal Lago and Hiroshi Unno. 2025. Artifact for \u201cOn Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs\u201d. doi:10.5281\/zenodo.16923662","DOI":"10.5281\/zenodo.16923662"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","unstructured":"Taro Sekiyama and Atsushi Igarashi. 2019. Handling Polymorphic Algebraic Effects. In Programming Languages and Systems - 28th European Symposium on Programming ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2019 Proceedings. 353\u2013380. doi:10.1007\/978-3-030-17184-1_13","DOI":"10.1007\/978-3-030-17184-1_13"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408999"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689805"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","unstructured":"Christian Skalka Scott F. Smith and David Van Horn. 2008. Types and trace effects of higher order programs. J. Funct. Program. 18 2 (2008) 179\u2013249. doi:10.1017\/S0956796807006466","DOI":"10.1017\/S0956796807006466"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_5"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"Hayo Thielecke. 2003. From control effects to typed continuation passing. In Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 139\u2013149. doi:10.1145\/640128.604144","DOI":"10.1145\/640128.604144"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_24"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","unstructured":"Nicolas Wu Tom Schrijvers and Ralf Hinze. 2014. Effect handlers in scope. In Proceedings of the 2014 ACM SIGPLAN symposium on Haskell Haskell 2014. 1\u201312. doi:10.1145\/2633357.2633358","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409022"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674641"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704886"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428207"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656433"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763184","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763184","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:04:14Z","timestamp":1784196254000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763184"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":69,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763184"],"URL":"https:\/\/doi.org\/10.1145\/3763184","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}