{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:10:41Z","timestamp":1784200241238,"version":"3.55.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-21-C-4023,HR00112590130"],"award-info":[{"award-number":["N66001-21-C-4023,HR00112590130"]}],"id":[{"id":"10.13039\/100000185","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":[[2025,10,9]]},"abstract":"<jats:p>\n                    Linear type systems are powerful because they can statically ensure the correct management of resources like memory, but they can also be cumbersome to work with, since even benign uses of a resource require that it be explicitly threaded through during computation.\n                    <jats:italic toggle=\"yes\">Borrowing<\/jats:italic>\n                    , as popularized by Rust, reduces this burden by allowing one to temporarily disable certain resource permissions (e.g., deallocation or mutation) in exchange for enabling certain structural permissions (e.g., weakening or contraction). In particular, this mechanism spares the borrower of a resource from having to explicitly return it to the lender but nevertheless ensures that the lender eventually reclaims ownership of the resource.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we elucidate the semantics of borrowing by starting with a standard linear type system for ensuring safe manual memory management in an untyped lambda calculus and gradually augmenting it with immutable borrows, lexical lifetimes, reborrowing, and finally mutable borrows. We prove semantic type soundness for our Borrow Calculus (\n                    <jats:monospace>BoCa<\/jats:monospace>\n                    ) using Borrow Logic (\n                    <jats:italic toggle=\"yes\">BoLo<\/jats:italic>\n                    ), a novel domain-specific separation logic for borrowing. We establish the soundness of this logic using a semantic model that additionally guarantees that our calculus is terminating and free of memory leaks. We also show that our Borrow Logic is robust enough to establish the semantic safety of some syntactically ill-typed programs that temporarily break but reestablish invariants.\n                  <\/jats:p>","DOI":"10.1145\/3764117","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3981-4007","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["From Linearity to Borrowing"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9434-0780","authenticated-orcid":false,"given":"Andrew","family":"Wagner","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8850-0984","authenticated-orcid":false,"given":"Olek","family":"Gierczak","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7744-4932","authenticated-orcid":false,"given":"Brianna","family":"Marshall","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2130-5092","authenticated-orcid":false,"given":"John M.","family":"Li","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7424-572X","authenticated-orcid":false,"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"issue":"4","key":"e_1_3_2_2_2","first-page":"397","article-title":"L3: a linear language with locations","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: a linear language with locations. Fundamenta Informaticae 77, 4 (2007), 397\u2013449.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/1037736"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_12"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290378"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_10"},{"key":"e_1_3_2_7_2","unstructured":"The Idris Community. 2020. !-notation. https:\/\/docs.idris-lang.org\/en\/latest\/tutorial\/interfaces.html#notation"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52592-0_60"},{"key":"e_1_3_2_9_2","first-page":"656","volume-title":"Proceedings of the ACM on Programming Languages","author":"Georges A\u00efna Linn","year":"2025","unstructured":"A\u00efna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A Eisenberg, Chris Casinghino, Fran\u00e7ois Pottier, and Derek Dreyer. 2025. Data Race Freedom \u00e0 la Mode. Proceedings of the ACM on Programming Languages 9, POPL (2025), 656\u2013686."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649842"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622798"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_16_2","article-title":"Type Universes as Allocation Effects","author":"Koronkevich Paulette","year":"2024","unstructured":"Paulette Koronkevich and William J Bowman. 2024. Type Universes as Allocation Effects. arXiv preprint arXiv:2407.06473 (2024).","journal-title":"arXiv preprint arXiv:2407.06473"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649848"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_22"},{"key":"e_1_3_2_22_2","article-title":"COGENT: certified compilation for a functional systems language","author":"O\u2019Connor Liam","year":"2016","unstructured":"Liam O\u2019Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby Murray. et al. 2016. COGENT: certified compilation for a functional systems language. arXiv preprint arXiv:1601.05520 (2016).","journal-title":"arXiv preprint arXiv:1601.05520"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_23"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.12"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"Daniel Patterson Noble Mushtak Andrew Wagner and Amal Ahmed. 2022. Semantic soundness for language interoperability. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 609\u2013624.","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.16"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408985"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","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.","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_3_2_31_2","unstructured":"John C Reynolds. 1983. Types abstraction and parametric polymorphism. In Information Processing 83 Proceedings of the IFIP 9th World Computer Congres. 513\u2013523."},{"key":"e_1_3_2_32_2","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Proceedings of the Scheme and Functional Programming Workshop. 81\u201392."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328486"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3735592"},{"key":"e_1_3_2_36_2","article-title":"Linear types can change the world!","volume":"3","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear types can change the world!. In Programming concepts and methods, Vol. 3. Citeseer, 5.","journal-title":"Programming concepts and methods"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689755"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3764117"},{"key":"e_1_3_2_39_2","unstructured":"Aaron Weiss Olek Gierczak Daniel Patterson and Amal Ahmed. 2021. Oxide: The Essence of Rust. arXiv:1903.00982 [cs.PL] https:\/\/arxiv.org\/abs\/1903.00982"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764117","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764117","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:14:16Z","timestamp":1784196856000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":38,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3764117"],"URL":"https:\/\/doi.org\/10.1145\/3764117","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}