{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T02:16:21Z","timestamp":1772158581918,"version":"3.50.1"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-21-1-0054"],"award-info":[{"award-number":["FA9550-21-1-0054"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004040","name":"KU Leuven","doi-asserted-by":"publisher","award":["C14\/18\/064"],"award-info":[{"award-number":["C14\/18\/064"]}],"id":[{"id":"10.13039\/501100004040","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":[[2022,4,29]]},"abstract":"<jats:p>\n            In 1995, Launchbury and Peyton Jones extended Haskell with an ST monad that allows the programmer to use higher-order mutable state. They informally argued that these state computations were safely encapsulated, and as such, that the rich reasoning principles stemming from the\n            <jats:italic>purity<\/jats:italic>\n            of the language, were not threatened.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we give a formal account of the preservation of\n            <jats:italic>purity<\/jats:italic>\n            after adding an ST monad to a simply-typed call-by-value recursive lambda calculus. We state and prove full abstraction when embedding the pure language into its extension with ST; contextual equivalences from the pure language continue to hold in the presence of ST.\n          <\/jats:p>\n          <jats:p>\n            Proving full abstraction of compilers is usually done by emulating or\n            <jats:italic>back-translating<\/jats:italic>\n            the target features (here: ST computations) into the source language, a well-known challenge in the secure compilation community. We employ a novel proof technique for proving our full abstraction result that allows us to use a semantically (but not syntactically) typed back-translation into an intermediate language. We believe that this technique provides additional insight into our proof and that it is of general interest to researchers studying programming languages and compilers using full abstraction.\n          <\/jats:p>\n          <jats:p>The results presented here are fully formalized in the Coq proof assistant using the Iris framework.<\/jats:p>","DOI":"10.1145\/3527326","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Purity of an ST monad: full abstraction by semantically typed back-translation"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1645-6876","authenticated-orcid":false,"given":"Koen","family":"Jacobs","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49255-0_70"},{"key":"e_1_2_1_2_1","volume-title":"Secure Internet Programming","author":"Abadi Mart\u00edn","unstructured":"Mart\u00edn Abadi . 1999. Protection in Programming-Language Translations . In Secure Internet Programming . Springer-Verlag . isbn:3-540-66130-1 Mart\u00edn Abadi. 1999. Protection in Programming-Language Translations. In Secure Internet Programming. Springer-Verlag. isbn:3-540-66130-1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00025"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837618"},{"key":"e_1_2_1_6_1","volume-title":"Simon Peyton Jones, and Philip Wadler","author":"Hudak Paul","year":"2007","unstructured":"Paul Hudak , John Hughes , Simon Peyton Jones, and Philip Wadler . 2007 . A History of Haskell: Being Lazy with Class. In History of Programming Languages . Paul Hudak, John Hughes, Simon Peyton Jones, and Philip Wadler. 2007. A History of Haskell: Being Lazy with Class. In History of Programming Languages."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6329773"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_2_1_9_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 ( 2018 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018)."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178246"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004154"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236768"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.011"},{"key":"e_1_2_1_15_1","unstructured":"Marco Patrignani. 2020. Why should anyone use colours? or syntax highlighting beyond code snippets. arXiv preprint arXiv:2001.11334.  Marco Patrignani. 2020. Why should anyone use colours? or syntax highlighting beyond code snippets. arXiv preprint arXiv:2001.11334."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434302"},{"key":"e_1_2_1_18_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT press . Benjamin C. Pierce. 2002. Types and programming languages. MIT press."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_2_1_20_1","volume-title":"CoqPL, Date: 2017\/01\/21-2017\/01\/21","author":"Timany Amin","unstructured":"Amin Timany , Robbert Krebbers , and Lars Birkedal . 2017. Logical relations in Iris . In CoqPL, Date: 2017\/01\/21-2017\/01\/21 , Location : Paris . Amin Timany, Robbert Krebbers, and Lars Birkedal. 2017. Logical relations in Iris. In CoqPL, Date: 2017\/01\/21-2017\/01\/21, Location: Paris."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_1_22_1","unstructured":"Philip Wadler. 1993. Monads for functional programming. In Program Design Calculi Manfred Broy (Ed.). Springer Berlin Heidelberg 233\u2013264. isbn:978-3-662-02880-3  Philip Wadler. 1993. Monads for functional programming. In Program Design Calculi Manfred Broy (Ed.). Springer Berlin Heidelberg 233\u2013264. isbn:978-3-662-02880-3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527326","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527326","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":22,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527326"],"URL":"https:\/\/doi.org\/10.1145\/3527326","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}