{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T20:36:21Z","timestamp":1770237381603,"version":"3.49.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"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, JP20H00582, JP20H05703, JP22K17875, JP24H00699"],"award-info":[{"award-number":["JP19K20247, JP20H00582, JP20H05703, JP22K17875, JP24H00699"]}],"id":[{"id":"10.13039\/501100001691","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,8,15]]},"abstract":"<jats:p>Many effect systems for algebraic effect handlers are designed to guarantee that all invoked effects are handled adequately. However, respective researchers have developed their own effect systems that differ in how to represent the collections of effects that may happen. This situation results in blurring what is required for the representation and manipulation of effect collections in a safe effect system.<\/jats:p>\n                  <jats:p>\n                    In this work, we present a language\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msub>\n                          <mml:mi>\u03bb<\/mml:mi>\n                          <mml:mi fontfamily=\"Georgia\" mathvariant=\"normal\">EA<\/mml:mi>\n                        <\/mml:msub>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    equipped with an effect system that abstracts the existing effect systems for algebraic effect handlers. The effect system of\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msub>\n                          <mml:mi>\u03bb<\/mml:mi>\n                          <mml:mi>EA<\/mml:mi>\n                        <\/mml:msub>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    is parameterized over\n                    <jats:italic toggle=\"yes\">effect algebras<\/jats:italic>\n                    , which abstract the representation and manipulation of effect collections in safe effect systems. We prove the type-and-effect safety of\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msub>\n                          <mml:mi>\u03bb<\/mml:mi>\n                          <mml:mi>EA<\/mml:mi>\n                        <\/mml:msub>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    by assuming that a given effect algebra meets certain properties called\n                    <jats:italic toggle=\"yes\">safety conditions<\/jats:italic>\n                    . As a result, we can obtain the safety properties of a concrete effect system by proving that an effect algebra corresponding to the concrete system meets the safety conditions. We also show that effect algebras meeting the safety conditions are expressive enough to accommodate some existing effect systems, each of which represents effect collections in a different style. Our framework can also differentiate the safety aspects of the effect collections of the existing effect systems. To this end, we extend\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msub>\n                          <mml:mi>\u03bb<\/mml:mi>\n                          <mml:mi>EA<\/mml:mi>\n                        <\/mml:msub>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    and the safety conditions to\n                    <jats:italic toggle=\"yes\">lift coercions<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">type-erasure semantics<\/jats:italic>\n                    , propose other effect algebras including ones for which no effect system has been studied in the literature, and compare which effect algebra is safe and which is not for the extensions.\n                  <\/jats:p>","DOI":"10.1145\/3674641","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"455-484","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Abstracting Effect Systems for Algebraic Effect Handlers"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-5949-6288","authenticated-orcid":false,"given":"Takuma","family":"Yoshioka","sequence":"first","affiliation":[{"name":"Kyoto University, Kyoto, 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 &amp; SOKENDAI, Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[{"name":"Kyoto University, Kyoto, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_1"},{"key":"e_1_3_2_4_1","unstructured":"Andrej Bauer and Matija Pretnar. 2021. Eff version 5.1. https:\/\/www.eff-lang.org\/"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0040253"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110257"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02283036"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2017.13"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99603"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.18"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2020.15"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_17"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000320"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3633280"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_2_25_1","unstructured":"Daan Leijen. 2018. Algebraic Effect Handlers with Resources and Deep Finalization. Technical Report MSR-TR-2018-10. 35 pages. https:\/\/www.microsoft.com\/en-us\/research\/publication\/algebraic-effect-handlers-resources-deep-finalization\/"},{"key":"e_1_3_2_26_1","unstructured":"Daan Leijen. 2024. Koka: a Functional Language with Effects version 3.1.0. https:\/\/koka-lang.github.io\/"},{"key":"e_1_3_2_27_1","unstructured":"Sam Lindley Daniel Hillerstr\u00f6m Simon Fowler James Cheney Jan Stolarek Frank Emrich Rudi Horn Vashti Galpin Wilmer Ricciotti and Philip Wadler. 2023. Links: Linking Theory to Practice for the Web version 0.9.8. https:\/\/links-lang.org\/"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481868"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290325"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27810-0_1"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:21)2014"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/186677.186689"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_12"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523710"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_13"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408999"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_5"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632896"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429074"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90018-D"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289429"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408981"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563289"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674641","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674641","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:49:06Z","timestamp":1770191346000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674641"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":52,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674641"],"URL":"https:\/\/doi.org\/10.1145\/3674641","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}