{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T01:48:31Z","timestamp":1784166511658,"version":"3.55.0"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Engineering and Physical Sciences Research Council","award":["EP\\\/T013516\\\/1"],"award-info":[{"award-number":["EP\\\/T013516\\\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Ownership and borrowing systems, designed to enforce safe memory management without the need for garbage collection, have been brought to the fore by the Rust programming language. Rust also aims to bring some guarantees offered by functional programming into the realm of performant systems code, but the type system is largely separate from the ownership model, with type and borrow checking happening in separate compilation phases. Recent models such as RustBelt and Oxide aim to formalise Rust in depth, but there is less focus on integrating the basic ideas into more traditional type systems. An approach designed to expose an essential core for ownership and borrowing would open the door for functional languages to borrow concepts found in Rust and other ownership frameworks, so that more programmers can enjoy their benefits.<\/jats:p>\n          <jats:p>One strategy for managing memory in a functional setting is through uniqueness types, but these offer a coarse-grained view: either a value has exactly one reference, and can be mutated safely, or it cannot, since other references may exist. Recent work demonstrates that linear and uniqueness types can be combined in a single system to offer restrictions on program behaviour and guarantees about memory usage. We develop this connection further, showing that just as graded type systems like those of Granule and Idris generalise linearity, a Rust-like ownership model arises as a graded generalisation of uniqueness. We combine fractional permissions with grading to give the first account of ownership and borrowing that smoothly integrates into a standard type system alongside linearity and graded types, and extend Granule accordingly with these ideas.<\/jats:p>","DOI":"10.1145\/3649848","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"1040-1070","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Functional Ownership through Fractional Uniqueness"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4284-3757","authenticated-orcid":false,"given":"Daniel","family":"Marshall","sequence":"first","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom \/ University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053373"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022251"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622843"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563319"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_9"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40355-2_13"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.22.3"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3609027.3609408"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.006"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029873.1029883"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/118014.117975"},{"key":"e_1_2_1_32_1","volume-title":"5th International Workshop on Trends in Linear Logic and Applications (TLLA","author":"Hughes Jack","year":"2021","unstructured":"Jack Hughes, Daniel Marshall, James Wood, and Dominic Orchard. 2021. Linear Exponentials as Graded Modal Types. In 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021). Rome (virtual), Italy. https:\/\/hal-lirmm.ccsd.cnrs.fr\/lirmm-03271465"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.353.6"},{"key":"e_1_2_1_34_1","unstructured":"Harley Eades III and Dominic Orchard. 2020. Grading Adjoint Logic. arxiv:2006.08854."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99623"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Anton Lorenzen Daan Leijen and Wouter Swierstra. 2023. FP^2: Fully in-Place Functional Programming. In ICFP\u201923. https:\/\/doi.org\/10.1145\/3607840 preprint 10.1145\/3607840","DOI":"10.1145\/3607840"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Dhruv C Makwana and Neel Krishnaswami. 2019. NumLin: Linear Types for Linear Algebra. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2019.14 10.4230\/LIPICS.ECOOP.2019.14","DOI":"10.4230\/LIPICS.ECOOP.2019.14"},{"key":"e_1_2_1_41_1","volume-title":"Graded Modal Types for Integrity and Confidentiality. In 17th Workshop on Programming Languages and Analysis for Security (PLAS","author":"Marshall Daniel","year":"2022","unstructured":"Daniel Marshall and Dominic Orchard. 2022. Graded Modal Types for Integrity and Confidentiality. In 17th Workshop on Programming Languages and Analysis for Security (PLAS 2022). arxiv:2309.04324."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.5"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.356.1"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Daniel Marshall and Dominic Orchard. 2024. Functional Ownership through Fractional Uniqueness (Appendix). https:\/\/doi.org\/10.5281\/zenodo.10799026 10.5281\/zenodo.10799026","DOI":"10.5281\/zenodo.10799026"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Daniel Marshall and Dominic Orchard. 2024. Functional Ownership through Fractional Uniqueness (Artefact). https:\/\/doi.org\/10.5281\/zenodo.10797791 10.5281\/zenodo.10797791","DOI":"10.5281\/zenodo.10797791"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_13"},{"key":"e_1_2_1_47_1","unstructured":"Conor McBride. 2001. The Derivative of a Regular Type is its Type of One-Hole Contexts. Unpublished manuscript 74\u201388. http:\/\/strictlypositive.org\/diff.pdf"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","unstructured":"Conor McBride. 2016. I Got Plenty o\u2019 Nuttin\u2019. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday 207\u2013233. https:\/\/doi.org\/10.1007\/978-3-319-30936-1_12 10.1007\/978-3-319-30936-1_12","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_4"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682100023X"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3342537"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3443420"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408985"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57787-4_23"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00068-4"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547626"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926436"},{"key":"e_1_2_1_62_1","volume-title":"Harley Eades III, and Dominic Orchard","author":"Vollmer Victoria","year":"2024","unstructured":"Victoria Vollmer, Daniel Marshall, Harley Eades III, and Dominic Orchard. 2024. A Mixed Linear and Graded Logic: Proofs, Terms, and Models. arxiv:2401.17199."},{"key":"e_1_2_1_63_1","first-page":"5","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. 3, 5. https:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/linear\/linear.dvi","journal-title":"Programming Concepts and Methods."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58027-1_24"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/363911.363923"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_1_67_1","volume-title":"Oxide: The Essence of Rust. 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."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_14"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649848","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649848","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:07Z","timestamp":1750287247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649848"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":69,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649848"],"URL":"https:\/\/doi.org\/10.1145\/3649848","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}