{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T06:19:37Z","timestamp":1790835577730,"version":"4.1.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>Purely functional programming languages pride themselves with reifying effects that are implicit in imperative languages into reusable and composable abstractions such as monads. This reification allows for more exact control over effects as well as the introduction of new or derived effects. However, despite libraries of more and more powerful abstractions over effectful operations being developed, syntactically the common 'do' notation still lags behind equivalent imperative code it is supposed to mimic regarding verbosity and code duplication. In this paper, we explore extending 'do' notation with other imperative language features that can be added to simplify monadic code: local mutation, early return, and iteration. We present formal translation rules that compile these features back down to purely functional code, show that the generated code can still be reasoned over using an implementation of the translation in the Lean 4 theorem prover, and formally prove the correctness of the translation rules relative to a simple static and dynamic semantics in Lean.<\/jats:p>","DOI":"10.1145\/3547640","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"512-539","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["\u2018do\u2019 unchained: embracing local imperativity in a purely functional language (functional pearl)"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2777-8117","authenticated-orcid":false,"given":"Sebastian","family":"Ullrich","sequence":"first","affiliation":[{"name":"KIT, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5158-4726","authenticated-orcid":false,"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14675-1_2"},{"key":"e_1_2_1_4_1","unstructured":"Niklas B\u00fclow. 2022. Proof Visualization for the Lean 4 Theorem Prover. https:\/\/pp.ipd.kit.edu\/publication.php?id=b \t\t\t\t  Niklas B\u00fclow. 2022. Proof Visualization for the Lean 4 Theorem Prover. https:\/\/pp.ipd.kit.edu\/publication.php?id=b"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581693"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007291"},{"key":"e_1_2_1_11_1","volume-title":"Aeneas: Rust Verification by Functional Translation.","author":"Ho Son","year":"2022","unstructured":"Son Ho and Jonathan Protzenko . 2022 . Aeneas: Rust Verification by Functional Translation. (2022). To appear at International Conference on Functional Programming (ICFP) . Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust Verification by Functional Translation. (2022). To appear at International Conference on Functional Programming (ICFP)."},{"key":"e_1_2_1_12_1","volume-title":"Haskell 98 language and libraries: the revised report","author":"Jones Simon Peyton","unstructured":"Simon Peyton Jones . 2003. Haskell 98 language and libraries: the revised report . Cambridge University Press . Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202532"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.153.8"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976007"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62034-6_48"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507664"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61055-3_27"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3426425.3426940"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73562"},{"key":"e_1_2_1_25_1","volume-title":"Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis","author":"Ullrich Sebastian","unstructured":"Sebastian Ullrich . 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis . Karlsruher Institut f\u00fcr Technologie (KIT) . https:\/\/pp.ipd.kit.edu\/publication.php?id=ullrich16masterarbeit Sebastian Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis. Karlsruher Institut f\u00fcr Technologie (KIT). https:\/\/pp.ipd.kit.edu\/publication.php?id=ullrich16masterarbeit"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:1)2022"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6684085"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001560"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547640","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547640","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547640"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":29,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547640"],"URL":"https:\/\/doi.org\/10.1145\/3547640","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}