{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:49Z","timestamp":1780994749936,"version":"3.54.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"DFG","award":["TH 665\/11-2"],"award-info":[{"award-number":["TH 665\/11-2"]}]}],"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>Session types provide a formal framework to enforce rich  \ncommunication protocols, ensuring correctness properties such as  \ntype safety and deadlock freedom. However, the traditional API of  \nfunctional session type systems with first-class channels often leads to problems  \nwith modularity and composability.<\/jats:p>\n          <jats:p>This paper proposes a new, alternative session type  \nAPI based on borrowing, embodied in the core calculus BGV. The  \nborrowing-based API enables building modular and composable code for session type  \nclients without imposing clutter or undue limitations. Its basis is a novel type  \nsystem, founded on ordered linear typing, for functional session  \ntypes with an explicit operation for splitting ownership of  \nchannels. We establish the semantics of BGV via a type-preserving translation to PGV,  \na deadlock-free functional  \nsession type calculus. We establish type safety and deadlock freedom  \nfor BGV by this translation.<\/jats:p>\n          <jats:p>We also present an external version of BGV that supports use  \nof borrow notation. We developed an algorithmic version of the type system that  \nincludes a mechanized verified translation from the external language to  \nBGV. This part establishes decidable type checking.<\/jats:p>","DOI":"10.1145\/3763173","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"3426-3453","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Borrowing from Session Types"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-7014-754X","authenticated-orcid":false,"given":"Hannes","family":"Saffrich","sequence":"first","affiliation":[{"name":"University of Freiburg, Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4510-2003","authenticated-orcid":false,"given":"Janek","family":"Spaderna","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9000-1239","authenticated-orcid":false,"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9539-8861","authenticated-orcid":false,"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisbon, Portugal"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1002\/MALQ.19900360405"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(99)00014-7"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604185"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2017.1"},{"key":"e_1_2_2_5_1","volume-title":"Vasconcelos","author":"Almeida Bernardo","year":"2021","unstructured":"Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos. 2021. Polymorphic Context-free Session Types. CoRR, abs\/2106.06658 (2021), arXiv:2106.06658. arxiv:2106.06658"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2022.104948"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000218"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656434"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2021.36"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290341"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563318"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(4:12)2015"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49099-X_6"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_2_20_1","volume-title":"Vasconcelos","author":"Gay Simon J.","year":"2025","unstructured":"Simon J. Gay and Vasco T. Vasconcelos. 2025. Session types. Cambridge University Press."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR. https:\/\/doi.org\/10.1007\/3-540-57208-2_35 10.1007\/3-540-57208-2_35","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2018.08.005"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.69.6"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498662"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(4:28)2023"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.2307\/2310058"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/012"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","unstructured":"Sam Lindley and J. Garrett Morris. 2016. Talking bananas: structural recursion for session types. In ICFP. https:\/\/doi.org\/10.1145\/2951913.2951921 10.1145\/2951913.2951921","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_32_1","volume-title":"Behavioural Types: from Theory to Tools, Simon Gay and Ant\u00f3nio Ravara (Eds.)","author":"Lindley Sam","unstructured":"Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools, Simon Gay and Ant\u00f3nio Ravara (Eds.). River Publishers. Extended version at https:\/\/homepages.inf.ed.ac.uk\/slindley\/papers\/fst-extended.pdf"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24836-1_5"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000289"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19195-9_1"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604147"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_21"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80088-4"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411290"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_16"},{"key":"e_1_2_2_44_1","volume-title":"Session Types in Haskell: Updating Message Passing for the 21st Century","author":"Sackman Matthew","year":"2015","unstructured":"Matthew Sackman and Susan Eisenbach. 2008. Session Types in Haskell: Updating Message Passing for the 21st Century. Imperial College, London. https:\/\/web.archive.org\/web\/20151017175211\/http:\/\/pubs.doc.ic.ac.uk\/session-types-in-haskell\/session-types-in-haskell.pdf"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689763"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","unstructured":"Hannes Saffrich Yuki Nishida and Peter Thiemann. 2024. Law and Order for Typestate with Borrowing. https:\/\/doi.org\/10.48550\/arXiv.2408.14031 arxiv:2408.14031. 10.48550\/arXiv.2408.14031","DOI":"10.48550\/arXiv.2408.14031"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16910888"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:33)2022"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3610612.3610624"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","unstructured":"Kaku Takeuchi Kohei Honda and Makoto Kubo. 1994. An Interaction-based Language and its Typing System. In PARLE. https:\/\/doi.org\/10.1007\/3-540-58184-7_118 10.1007\/3-540-58184-7_118","DOI":"10.1007\/3-540-58184-7_118"},{"key":"e_1_2_2_51_1","unstructured":"The Rust Team. 2024. The Rust Programming Language. http:\/\/rust-lang.org\/"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951926"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2006.06.028"},{"issue":"2","key":"e_1_2_2_55_1","first-page":"2","article-title":"Linear Types can Change the World!. In Programming concepts and methods","volume":"2","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear Types can Change the World!. In Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990. North-Holland, 561.","journal-title":"Proceedings of the IFIP Working Group"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763173","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:41:14Z","timestamp":1760031674000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763173"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":56,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763173"],"URL":"https:\/\/doi.org\/10.1145\/3763173","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","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"}}]}}