{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:20Z","timestamp":1787592320462,"version":"build-2736575974"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Destination passing \u2014aka. out parameters\u2014 is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3720423","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"253-279","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Destination Calculus: A Linear \ud835\udf06-Calculus for Purely Functional Memory Writes"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-8700-2741","authenticated-orcid":false,"given":"Thomas","family":"Bagrel","sequence":"first","affiliation":[{"name":"Tweag, OSPO, Paris, France"},{"name":"LORIA, FM - Department of Formal Methods, Team MOSEL\/VERIDIS, Villers-l\u00e8s-Nancy, France"},{"name":"Inria, Team MOSEL\/VERIDIS, Villers-l\u00e8s-Nancy, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5985-2086","authenticated-orcid":false,"given":"Arnaud","family":"Spiwack","sequence":"additional","affiliation":[{"name":"Tweag, OSPO, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_1_4_1","volume-title":"35es Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2024)","author":"Bagrel Thomas","year":"2024","unstructured":"Thomas Bagrel. 2024. Destination-passing style programming: a Haskell implementation. In 35es Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2024). Saint-Jacut-de-la-Mer, France. https:\/\/inria.hal.science\/hal-04406360"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Thomas Bagrel and Arnaud Spiwack. 2025. Destination calculus: Progress and Preservation proofs using Coq proof assistant. doi:10.5281\/zenodo.14982363","DOI":"10.5281\/zenodo.14982363"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Jean-Philippe Bernardy Mathieu Boespflug Ryan R. Newton Simon Peyton Jones and Arnaud Spiwack. 2018. Linear Haskell: practical linearity in a higher-order polymorphic language. Proceedings of the ACM on Programming Languages 2 POPL (Jan. 2018) 1\u201329. arXiv:1710.09756 [cs]. doi:10.1145\/3158093","DOI":"10.1145\/3158093"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.028"},{"key":"e_1_3_1_8_1","unstructured":"Fr\u00e9d\u00e9ric Bour Basile Cl\u00e9ment and Gabriel Scherer. 2021. Tail Modulo Cons. arXiv:2102.09823 [cs] (Feb. 2021). http:\/\/arxiv.org\/abs\/2102.09823 arXiv: 2102.09823."},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v11i26.21851"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.29"},{"key":"e_1_3_1_12_1","volume-title":"The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages","author":"Felleisen Matthias","year":"1987","unstructured":"Matthias Felleisen. 1987. The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages. phd. Indiana University, USA. AAI8727494. https:\/\/www2.ccs.neu.edu\/racket\/pubs\/dissertation-felleisen.pdf"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_1_14_1","unstructured":"Jeremy Gibbons. 1993. Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips. No. 71 (1993). Number: No. 71. https:\/\/www.cs.ox.ac.uk\/publications\/publication2363-abstract.html"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3609025.3609479"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90030-2"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90059-1"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571233"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607840"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656398"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268953"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351253"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3443420"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"F. Pfenning and H. C. Wong. 1995. On a Modal \ud835\udf06-Calculus for S4. Electronic Notes in Theoretical Computer Science 1 (Jan. 1995) 515\u2013534. doi:10.1016\/S1571-0661(04)00028-3","DOI":"10.1016\/S1571-0661(04)00028-3"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291155"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122948.3122949"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547626"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720423","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720423","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:32:12Z","timestamp":1787589132000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720423"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":27,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720423"],"URL":"https:\/\/doi.org\/10.1145\/3720423","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}