{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:19Z","timestamp":1780994479096,"version":"3.54.1"},"reference-count":55,"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\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["Future Leaders Fellowship MR\/T043830\/1 (EHOP)"],"award-info":[{"award-number":["Future Leaders Fellowship MR\/T043830\/1 (EHOP)"]}],"id":[{"id":"10.13039\/100014013","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>\n                    Programmers can often improve the performance of their programs by reducing heap allocations: either by allocating on the stack or reusing existing memory in-place. However, without safety guarantees, these optimizations can easily lead to use-after-free errors and even type unsoundness. In this paper, we present a design based on\n                    <jats:italic toggle=\"yes\">modes<\/jats:italic>\n                    which allows programmers to safely reduce allocations by using stack allocation and in-place updates of immutable structures. We focus on three mode axes: affinity, uniqueness and locality. Modes are fully backwards compatible with existing OCaml code and can be completely inferred. Our work makes manual memory management in OCaml safe and convenient and charts a path towards bringing the benefits of Rust to OCaml.\n                  <\/jats:p>","DOI":"10.1145\/3674642","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"485-514","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Oxidizing OCaml with Modal Memory Management"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3538-9688","authenticated-orcid":false,"given":"Anton","family":"Lorenzen","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-7046-3035","authenticated-orcid":false,"given":"Leo","family":"White","sequence":"additional","affiliation":[{"name":"Jane Street, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4609-9101","authenticated-orcid":false,"given":"Stephen","family":"Dolan","sequence":"additional","affiliation":[{"name":"Jane Street, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7669-9781","authenticated-orcid":false,"given":"Richard A.","family":"Eisenberg","sequence":"additional","affiliation":[{"name":"Jane Street, NYC, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1360-4714","authenticated-orcid":false,"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"Danel Ahman. 2023. When Programs Have to Watch Paint Dry. In FoSSaCS. 1\u201323. https:\/\/doi.org\/10.1007\/978-3-031-30829-1_1 10.1007\/978-3-031-30829-1_1","DOI":"10.1007\/978-3-031-30829-1_1"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Robert Atkey. 2018.Syntax and semantics of quantitative type theory.In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. 56\u201365. https:\/\/doi.org\/10.1145\/3209108.3209189 10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Erik Barendsen and Sjaak Smetsers. 1995. Uniqueness Type Inference. In Proceedings of the 7th International Symposium on Programming Languages: Implementations Logics and Programs. 189\u2013206. https:\/\/doi.org\/10.1007\/BFb0026821 10.1007\/BFb0026821","DOI":"10.1007\/BFb0026821"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_3_2_7_1","unstructured":"Aria Beingessner Steve Klabnik and Yuki Okushi. 2017. Higher-Rank Trait Bounds (HRTBs) (The Rustonomicon sec. 3.7). https:\/\/doc.rust-lang.org\/nomicon\/hrtb.html."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788785"},{"key":"e_1_3_2_9_1","first-page":"121","volume-title":"International Workshop on Computer Science Logic","author":"Benton P Nick","year":"1994","unstructured":"P Nick Benton. 1994. A mixed linear and non-linear logic: Proofs, terms and models. In International Workshop on Computer Science Logic. Springer, 121\u2013135."},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Edwin Brady. 2021. Idris 2: Quantitative type theory in practice. arXiv preprint arXiv:2104.00480 (2021). https:\/\/doi.org\/10.48550\/arXiv.2104.00480 10.48550\/arXiv.2104.00480","DOI":"10.48550\/arXiv.2104.00480"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_2_13_1","volume-title":"Compile time garbage collection","author":"Bruynooghe Maurice","year":"1986","unstructured":"Maurice Bruynooghe. 1986. Compile time garbage collection. Katholieke Universiteit Leuven. Departement Computerwetenschappen."},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133896"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"William D Clinger. 1998. Proper tail recursion and space efficiency. In Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation. 174\u2013185. https:\/\/doi.org\/10.1145\/277650.277719 10.1145\/277650.277719","DOI":"10.1145\/277650.277719"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_12"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837652"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_12"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57840-4_34"},{"key":"e_1_3_2_21_1","unstructured":"Damien Doligez. 2016. Unboxed types. Pull request against OCaml source. https:\/\/github.com\/ocaml\/ocaml\/pull\/606"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-39197-3_7"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301665"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Daniel Gratzer GA Kavvos Andreas Nuyts and Lars Birkedal. 2020. Multimodal dependent type theory. In Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science. 492\u2013506. https:\/\/doi.org\/10.1145\/3373718.3394736 10.1145\/3373718.3394736","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_3_2_26_1","unstructured":"Junyoung Jang Sophia Roshal Frank Pfenning and Brigitte Pientka. 2024. Adjoint Natural Deduction (Extended Version). CoRR abs\/2402.01428 (2024)."},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_6"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Neelakantan R. Krishnaswami C\u00e9cilia Pradic and Nick Benton. 2015. Integrating Linear and Dependent Types. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2775051.2676969 10.1145\/2775051.2676969 http:\/\/www.cs.bham.ac.uk\/~krishnan\/dlnlpaper.pdf.","DOI":"10.1145\/2775051.2676969"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27683-0_16"},{"key":"e_1_3_2_31_1","first-page":"265","volume-title":"Behavioural Types: from Theory to Tools","author":"Lindley Sam","year":"2017","unstructured":"Sam Lindley and J Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools. River Publishers, 265\u2013286."},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607840"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_13"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708027"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022670.2951925"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Young Gil Park and Benjamin Goldberg. 1992. Escape analysis on lists. In Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation. 116\u2013127. https:\/\/doi.org\/10.1145\/143103.143125 10.1145\/143103.143125","DOI":"10.1145\/143103.143125"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500598"},{"key":"e_1_3_2_41_1","unstructured":"Klaas Pruiksma William Chargin Frank Pfenning and Jason Reed. 2018. Adjoint logic. Unpublished manuscript April (2018)."},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Alex Reinking Ningning Xie Leonardo de Moura and Daan Leijen. 2021. Perceus: Garbage free reference counting with reuse. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 96\u2013111. https:\/\/doi.org\/10.1145\/3453483.3454032 10.1145\/3453483.3454032","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Michael Shulman. 2023. Semantics of multimodal adjoint type theory. arXiv preprint arXiv:2303.02572 (2023). https:\/\/doi.org\/10.48550\/arXiv.2303.02572 10.48550\/arXiv.2303.02572","DOI":"10.48550\/arXiv.2303.02572"},{"key":"e_1_3_2_44_1","unstructured":"Arnaud Spiwack. 2018. Linear types. A GHC Proposal. https:\/\/github.com\/ghc-proposals\/ghc-proposals\/blob\/master\/proposals\/0111-linear-types.rst"},{"key":"e_1_3_2_45_1","unstructured":"Arnaud Spiwack. 2023. Linear constraints proposal. A GHC Proposal. https:\/\/github.com\/tweag\/ghc-proposals\/blob\/linear-constraints\/proposals\/0621-linear-constraints.rst"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547626"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632896"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"key":"e_1_3_2_49_1","unstructured":"Mads Tofte Lars Birkedal Martin Elsman Niels Hallenberg Tommy H\u00f8jfeld Olesen and Peter Sestoft. 2002. Programming with regions in the ML Kit (for version 4). IT University of Copenhagen."},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","unstructured":"Cassia Torczon Emmanuel Suarez Acevedo Shubh Agrawal Joey Velez-Ginorio and Stephanie Weirich. 2023. Effects and Coeffects in Call-By-Push-Value (Extended Version). arXiv preprint arXiv:2311.11795 (2023). https:\/\/doi.org\/10.48550\/arXiv.2311.11795 10.48550\/arXiv.2311.11795","DOI":"10.48550\/arXiv.2311.11795"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926436"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","unstructured":"Sebastian Ullrich and Leonardo de Moura. 2019. Counting immutable beans: Reference counting optimized for purely functional programming. In Proceedings of the 31st Symposium on Implementation and Application of Functional Languages. 1\u201312. https:\/\/doi.org\/10.1145\/3412932.3412935 10.1145\/3412932.3412935","DOI":"10.1145\/3412932.3412935"},{"key":"e_1_3_2_54_1","first-page":"3","article-title":"Substructural type systems","author":"Walker David","year":"2005","unstructured":"David Walker. 2005. Substructural type systems. Advanced topics in types and programming languages (2005), 3\u201344.","journal-title":"Advanced topics in types and programming languages"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_14"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674642","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674642","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:49:02Z","timestamp":1770191342000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674642"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":55,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674642"],"URL":"https:\/\/doi.org\/10.1145\/3674642","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"}}]}}