{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:55:30Z","timestamp":1770274530380,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1909517"],"award-info":[{"award-number":["CCF-1909517"]}],"id":[{"id":"10.13039\/100000001","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":[[2023,10,16]]},"abstract":"<jats:p>We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect typing. This serves as a simple model of the integration of an effect typing discipline with an existing effectful typed language that does not track fine-grained effect information. Our language supports a simple module system to model the programming model of gradual migration from unchecked to checked effect typing in the style of Typed Racket.<\/jats:p>\n          <jats:p>The surface language GrEff is given semantics by elaboration to a core language Core GrEff. We equip Core GrEff with an inequational theory for reasoning about the semantic error ordering and desired program equivalences for programming with effects and handlers. We derive an operational semantics for the language from the equations provable in the theory. We then show that the theory is sound by constructing an operational logical relations model to prove the graduality theorem. This extends prior work on embedding-projection pair models of gradual typing to handle effect typing and subtyping.<\/jats:p>","DOI":"10.1145\/3622860","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1758-1786","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Gradual Typing for Effect Handlers"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8141-195X","authenticated-orcid":false,"given":"Max S.","family":"New","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6871-1714","authenticated-orcid":false,"given":"Eric","family":"Giovannini","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0697-7405","authenticated-orcid":false,"given":"Daniel R.","family":"Licata","sequence":"additional","affiliation":[{"name":"Wesleyan University, Middletown, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP","author":"Asai Kenichi","year":"2005","unstructured":"Kenichi Asai . 2005. Logical relations for call-by-value delimited continuations . In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005 , Tallinn, Estonia , 23-24 September 2005, Marko C. J. D. van Eekelen (Ed.) (Trends in Functional Programming , Vol. 6). 63\u2013 78 . Kenichi Asai. 2005. Logical relations for call-by-value delimited continuations. In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005, Marko C. J. D. van Eekelen (Ed.) (Trends in Functional Programming, Vol. 6). 63\u201378."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628149"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005097"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000027"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290329"},{"key":"e_1_2_1_7_1","unstructured":"WasmFX Contributors. [n.d.]. WasmFX: Effect Handlers for WebAssembly. https:\/\/wasmfx.dev\/ Accessed: 2020-11-10. \t\t\t\t  WasmFX Contributors. [n.d.]. WasmFX: Effect Handlers for WebAssembly. https:\/\/wasmfx.dev\/ Accessed: 2020-11-10."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_12"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000121"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503791"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485503"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481868"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_1_22_1","volume-title":"Licata","author":"New Max S.","year":"2023","unstructured":"Max S. New , Eric Giovannini , and Daniel R . Licata . 2023 . Gradual Typing for Effect Handlers (Extended Version) . https:\/\/maxsnew.com\/docs\/greff-extended.pdf Max S. New, Eric Giovannini, and Daniel R. Licata. 2023. Gradual Typing for Effect Handlers (Extended Version). https:\/\/maxsnew.com\/docs\/greff-extended.pdf"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.24"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290328"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.30"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_11"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_1_30_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81\u201392","author":"Jeremy","unstructured":"Jeremy G. Siek and Walid Taha. 2006 . Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81\u201392 . Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81\u201392."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_14"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89159-6_21"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622860","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622860","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622860"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":38,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622860"],"URL":"https:\/\/doi.org\/10.1145\/3622860","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}