{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:54Z","timestamp":1775873514207,"version":"3.50.1"},"reference-count":58,"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\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP19K20247,JP22K17875,JP20H00582,JP20H04162,JP22H03564,JP20H05703,JP20K20625,JP22H03570"],"award-info":[{"award-number":["JP19K20247,JP22K17875,JP20H00582,JP20H04162,JP22H03564,JP20H05703,JP20K20625,JP22H03570"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003382","name":"Core Research for Evolutional Science and Technology","doi-asserted-by":"publisher","award":["JPMJCR21M3"],"award-info":[{"award-number":["JPMJCR21M3"]}],"id":[{"id":"10.13039\/501100003382","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            Algebraic effects and handlers are a mechanism to structure programs with computational effects in a modular way. They are recently gaining popularity and being adopted in practical languages, such as OCaml. Meanwhile, there has been substantial progress in program verification via\n            <jats:italic toggle=\"yes\">refinement type systems<\/jats:italic>\n            . While a variety of refinement type systems have been proposed, thus far there has not been a satisfactory refinement type system for algebraic effects and handlers. In this paper, we fill the void by proposing a novel refinement type system for languages with algebraic effects and handlers. The expressivity and usefulness of algebraic effects and handlers come from their ability to manipulate\n            <jats:italic toggle=\"yes\">delimited continuations<\/jats:italic>\n            , but delimited continuations also complicate programs' control flow and make their verification harder. To address the complexity, we introduce a novel concept that we call\n            <jats:italic toggle=\"yes\">answer refinement modification<\/jats:italic>\n            (ARM for short), which allows the refinement type system to precisely track what effects occur and in what order when a program is executed, and reflect such information as modifications to the refinements in the types of delimited continuations. We formalize our type system that supports ARM (as well as answer\n            <jats:italic toggle=\"yes\">type<\/jats:italic>\n            modification, or ATM) and prove its soundness. Additionally, as a proof of concept, we have extended the refinement type system to a subset of OCaml 5 which comes with a built-in support for effect handlers, implemented a type checking and inference algorithm for the extension, and evaluated it on a number of benchmark programs that use algebraic effects and handlers. The evaluation demonstrates that ARM is conceptually simple and practically useful.\n          <\/jats:p>\n          <jats:p>\n            Finally, a natural alternative to directly reasoning about a program with delimited continuations is to apply a\n            <jats:italic toggle=\"yes\">continuation passing style<\/jats:italic>\n            (CPS) transformation that transforms the program to a pure program without delimited continuations. We investigate this alternative in the paper, and show that the approach is indeed possible by proposing a novel CPS transformation for algebraic effects and handlers that enjoys bidirectional (refinement-)type-preservation. We show that there are pros and cons with this approach, namely, while one can use an existing refinement type checking and inference algorithm that can only (directly) handle pure programs, there are issues such as needing type annotations in source programs and making the inferred types less informative to a user.\n          <\/jats:p>","DOI":"10.1145\/3633280","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"115-147","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-4147-9572","authenticated-orcid":false,"given":"Fuga","family":"Kawamata","sequence":"first","affiliation":[{"name":"Waseda University, 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":"University of Tsukuba, Tsukuba, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5305-4916","authenticated-orcid":false,"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[{"name":"Waseda University, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158095"},{"key":"e_1_3_1_3_1","first-page":"10","volume-title":"Abstracts of the 21st Meeting \u2018Types for Proofs and Programs\u2019 (TYPES)","author":"Ahman Danel","year":"2015","unstructured":"Danel Ahman and Gordon Plotkin. 2015. Refinement types for algebraic effects. In Abstracts of the 21st Meeting \u2018Types for Proofs and Programs\u2019 (TYPES). Institute of Cybernetics, Tallinn University of Technology, 10\u201311."},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-009-9049-5"},{"key":"e_1_3_1_6_1","unstructured":"Andrej Bauer. 2018. What is algebraic about algebraic effects and handlers? CoRR abs\/1807.05923 (2018). arXiv:1807.05923 http:\/\/arxiv.org\/abs\/1807.05923"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_1"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/jjlamp.2014.02.001"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236764"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21314-4_4"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110257"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Timothy S. Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proceedings of the ACM SIGPLAN\u201991 Conference on Programming Language Design and Implementation (PLDI) Toronto Ontario Canada June 26-28 1991 David S. Wise (Ed.).ACM 268\u2013277. https:\/\/doi.org\/10.1145\/113445.113468 10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_1_22_1","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/978-3-030-02768-1_22","volume-title":"Programming Languages and Systems","author":"Hillerstr\u00f6m Daniel","year":"2018","unstructured":"Daniel Hillerstr\u00f6m and Sam Lindley. 2018. Shallow Effect Handlers. In Programming Languages and Systems, Sukyoung Ryu (Ed.). Springer International Publishing, Cham, 415\u2013435."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.18"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3564719.3568691"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000320"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958060"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Daan Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types. In Proceedings 5th Workshop on Mathematically Structured Functional Programming MSFP@ETAPS 2014 Grenoble France 12 April 2014 (EPTCS Vol. 153) Paul Blain Levy and Neel Krishnaswami (Eds.). 100\u2013126. https:\/\/doi.org\/10.4204\/EPTCS.153.8 10.4204\/EPTCS.153.8","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034786"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_3_1_34_1","unstructured":"Multicore OCaml. 2022. OCaml effects examples. Retrieved November 5 2022 from https:\/\/github.com\/ocaml-multicore\/effects-examples"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.30"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_1_39_1","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/978-3-642-00590-9_7","volume-title":"Programming Languages and Systems","author":"Plotkin Gordon","year":"2009","unstructured":"Gordon Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. In Programming Languages and Systems, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 80\u201394."},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_3_1_43_1","unstructured":"Matija Pretnar. 2022. Eff. Retrieved November 5 2022 from https:\/\/github.com\/matijapretnar\/eff"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706315"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604144"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158100"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429081"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908110"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_19"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633280","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3633280","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3633280","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:52Z","timestamp":1751659672000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633280"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":58,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3633280"],"URL":"https:\/\/doi.org\/10.1145\/3633280","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"}}]}}