{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:13:46Z","timestamp":1760044426859,"version":"3.41.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["2019\/33\/B\/ST6\/00289"],"award-info":[{"award-number":["2019\/33\/B\/ST6\/00289"]}],"id":[{"id":"10.13039\/501100004281","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,8,30]]},"abstract":"<jats:p>Effect handlers are a modern and increasingly popular approach to structuring computational effects in functional programming languages. However, while their traditional operational semantics is well-suited to implementation tasks, it is less ideal as a reduction theory. We therefore introduce a fine-grained reduction theory for deep effect handlers, inspired by our existing reduction theory for shift0, along with a standard reduction strategy. We relate this strategy to the traditional, non-local operational semantics via a simulation argument, and show that the reduction theory preserves observational equivalence with respect to the classical semantics of handlers, thus allowing its use as a rewriting theory for handler-equipped programming languages -- this rewriting system mostly coincides with previously studied type-based optimisations. In the process, we establish theoretical properties of our reduction theory, including confluence and standardisation theorems, adapting and extending existing techniques. Finally, we demonstrate the utility of our semantics by providing the first normalisation-by-evaluation algorithm for effect handlers, and prove its soundness and completeness. Additionally, we establish non-expressibility of the lift operator, found in some effect-handler calculi, by the other constructs.<\/jats:p>","DOI":"10.1145\/3607848","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"511-540","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A General Fine-Grained Reduction Theory for Effect Handlers"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5011-3458","authenticated-orcid":false,"given":"Filip","family":"Sieczkowski","sequence":"first","affiliation":[{"name":"Heriot-Watt University, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9978-9536","authenticated-orcid":false,"given":"Mateusz","family":"Pyzik","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1477-4635","authenticated-orcid":false,"given":"Dariusz","family":"Biernacki","sequence":"additional","affiliation":[{"name":"University of Wroc\u0142aw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation thesis"},{"volume-title":"A General Church-Rosser Theorem","author":"Aczel Peter","key":"e_1_2_1_2_1","unstructured":"Peter Aczel. 1978. A General Church-Rosser Theorem. University of Manchester."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950400427X"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.007"},{"volume-title":"The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics","author":"Barendregt Hendrik Pieter","key":"e_1_2_1_6_1","unstructured":"Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics, Vol. 103). North-Holland. isbn:978-0-444-86748-3"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64437-6_8"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:5)2005"},{"key":"e_1_2_1_10_1","volume-title":"An Operational Foundation for Delimited Continuations in the CPS Hierarchy. CoRR, abs\/cs\/0508048","author":"Biernacka Malgorzata","year":"2005","unstructured":"Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. 2005. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. CoRR, abs\/cs\/0508048 (2005), arXiv:cs\/0508048. arxiv:cs\/0508048"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.10"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3479394.3479399"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000039"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v11i26.21851"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006259"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"key":"e_1_2_1_23_1","volume-title":"Robert Bruce Findler, and Matthew Flatt","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press. isbn:978-0-262-06275-6 http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=11885"},{"key":"e_1_2_1_24_1","volume-title":"Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts - III","author":"Felleisen Matthias","year":"1986","unstructured":"Matthias Felleisen and Daniel P. Friedman. 1987. Control operators, the SECD-machine, and the \u03bb -calculus. In Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986, Martin Wirsing (Ed.). North-Holland, 193\u2013222. isbn:0-444-70253-9"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS \u201986)","author":"Felleisen Matthias","year":"1986","unstructured":"Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, and Bruce F. Duba. 1986. Reasoning with Continuations. In Proceedings of the Symposium on Logic in Computer Science (LICS \u201986), Cambridge, Massachusetts, USA, June 16-18, 1986. IEEE Computer Society, 131\u2013141."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2005026"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.05.011"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000085X"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000040"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039592"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485479"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_17"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2013.521"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034786"},{"key":"e_1_2_1_39_1","unstructured":"James McKinna. 2022. The Lambda Calculus Formalised: the Church-Rosser and Standardisation Theorems with Applications. https:\/\/www.macs.hw.ac.uk\/splv\/splv-2022\/ Unpublished Lecture Notes from the Scottish Programming Languages and Verification Summer School (SPLV 2022) Edinburgh"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.7488\/era"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19790250104"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.30"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"volume-title":"Theories of programming languages","author":"Reynolds John C.","key":"e_1_2_1_48_1","unstructured":"John C. Reynolds. 1998. Theories of programming languages. Cambridge University Press. isbn:978-0-521-59414-1"},{"volume-title":"Efficient Algebraic Effect Handlers. Ph. D. Dissertation. Arenberg Doctoral School","author":"Saleh Amr Hany","key":"e_1_2_1_49_1","unstructured":"Amr Hany Saleh. 2019. Efficient Algebraic Effect Handlers. Ph. D. Dissertation. Arenberg Doctoral School, Faculty of Engineering Science, KU Leuven, Belgium."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523710"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","unstructured":"Filip Sieczkowski Mateusz Pyzik and Dariusz Biernacki. 2023. A General Fine-Grained Reduction Theory for Effect Handlers: Formalisation. https:\/\/doi.org\/10.5281\/zenodo.7993545 10.5281\/zenodo.7993545","DOI":"10.5281\/zenodo.7993545"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-21551-7_14"},{"key":"e_1_2_1_54_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\/3607848","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607848","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607848"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":54,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607848"],"URL":"https:\/\/doi.org\/10.1145\/3607848","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}