{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:14Z","timestamp":1780994474697,"version":"3.54.1"},"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>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. Borrowing, 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.<\/jats:p>\n          <jats:p>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 (BoCa) using Borrow Logic (BoLo), 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.<\/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":2,"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":[{"key":"e_1_2_2_1_1","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_2_2_2_1","volume-title":"Semantics of types for mutable state","author":"Ahmed Amal Jamil","unstructured":"Amal Jamil Ahmed. 2004. Semantics of types for mutable state. Princeton University."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_12"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290378"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_10"},{"key":"e_1_2_2_6_1","unstructured":"The Idris Community. 2020. !-notation. https:\/\/docs.idris-lang.org\/en\/latest\/tutorial\/interfaces.html##notation"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52592-0_60"},{"key":"e_1_2_2_8_1","volume-title":"Proceedings of the ACM on Programming Languages, 9, POPL","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_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649842"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622798"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the ACM on Programming Languages, 2, POPL","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACM on Programming Languages, 2, POPL (2017), 1\u201334."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_15_1","unstructured":"Paulette Koronkevich and William J Bowman. 2024. Type Universes as Allocation Effects. arXiv preprint arXiv:2407.06473."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649848"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_22"},{"key":"e_1_2_2_21_1","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."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_23"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.12"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_2_2_26_1","volume-title":"Nominal logic, a first order theory of names and binding. Information and computation, 186, 2","author":"Pitts Andrew M","year":"2003","unstructured":"Andrew M Pitts. 2003. Nominal logic, a first order theory of names and binding. Information and computation, 186, 2 (2003), 165\u2013193."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.16"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408985"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the IFIP 9th World Computer Congres. 513\u2013523","author":"Reynolds John C","year":"1983","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_2_2_31_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop. 81\u201392","author":"Jeremy","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_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328486"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3735592"},{"key":"e_1_2_2_35_1","unstructured":"Philip Wadler. 1990. Linear types can change the world!. In Programming concepts and methods. 3 5."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689755"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3764117"},{"key":"e_1_2_2_38_1","volume-title":"Oxide: The Essence of Rust. arxiv:1903.00982. arxiv:1903.00982","author":"Weiss Aaron","year":"2021","unstructured":"Aaron Weiss, Olek Gierczak, Daniel Patterson, and Amal Ahmed. 2021. Oxide: The Essence of Rust. arxiv:1903.00982. arxiv: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":[[2025,10,9]],"date-time":"2025-10-09T17:41:49Z","timestamp":1760031709000},"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"}}]}}