{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T12:04:26Z","timestamp":1790683466534,"version":"4.1.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683289 and 101003349"],"award-info":[{"award-number":["683289 and 101003349"]}],"id":[{"id":"10.13039\/501100000781","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":[[2021,8,22]]},"abstract":"<jats:p>\n            The Rust language offers a promising approach to safe systems programming based on the principle of\n            <jats:italic>aliasing XOR mutability<\/jats:italic>\n            : a value may be\n            <jats:italic>either<\/jats:italic>\n            aliased\n            <jats:italic>or<\/jats:italic>\n            mutable, but not both at the same time. However, to implement pointer-based data structures with internal sharing, such as graphs or doubly-linked lists, we need to be able to mutate aliased state. To support such data structures, Rust provides a number of APIs that offer so-called\n            <jats:italic>interior mutability<\/jats:italic>\n            : the ability to mutate data via method calls on a shared reference. Unfortunately, the existing APIs sacrifice flexibility, concurrent access, and\/or performance, in exchange for safety.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we propose a new Rust API called GhostCell which avoids such sacrifices by\n            <jats:italic>separating permissions from data<\/jats:italic>\n            : it enables the user to safely synchronize access to a\n            <jats:italic>collection<\/jats:italic>\n            of data via a single permission. GhostCell repurposes an old trick from typed functional programming:\n            <jats:italic>branded types<\/jats:italic>\n            (as exemplified by Haskell\u2019s ST monad), which combine phantom types and rank-2 polymorphism to simulate a lightweight form of state-dependent types. We have formally proven the soundness of GhostCell by adapting and extending RustBelt, a semantic soundness proof for a representative subset of Rust, mechanized in Coq.\n          <\/jats:p>","DOI":"10.1145\/3473597","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["GhostCell: separating permissions from data in Rust"],"prefix":"10.1145","volume":"5","author":[{"given":"Joshua","family":"Yanovski","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hoang-Hai","family":"Dang","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_2_2_2_1","volume-title":"You can\u2019t spell trust without Rust. Master\u2019s thesis","author":"Beingessner Alexis"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749611"},{"key":"e_1_2_2_4_1","unstructured":"crossbeam. 2021. crossbeam. https:\/\/crates.io\/crates\/crossbeam  crossbeam. 2021. crossbeam. https:\/\/crates.io\/crates\/crossbeam"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512532"},{"key":"e_1_2_2_6_1","unstructured":"Nick Fitzgerald and Simon Sapin. 2020. The Typed-Arena library. https:\/\/crates.io\/crates\/typed-arena  Nick Fitzgerald and Simon Sapin. 2020. The Typed-Arena library. https:\/\/crates.io\/crates\/typed-arena"},{"key":"e_1_2_2_7_1","unstructured":"fixedbitset. 2021. fixedbitset. https:\/\/crates.io\/crates\/fixedbitset  fixedbitset. 2021. fixedbitset. https:\/\/crates.io\/crates\/fixedbitset"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006046"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_2_10_1","unstructured":"Brook Heisler and Jorge Aparicio. 2020. The Criterion library. https:\/\/crates.io\/crates\/criterion  Brook Heisler and Jorge Aparicio. 2020. The Criterion library. https:\/\/crates.io\/crates\/criterion"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the 1994 ACM Conference on LISP and Functional Programming. 196\u2013207","author":"Kfoury A. J."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.039"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_27"},{"key":"e_1_2_2_23_1","unstructured":"Nicholas D. Matsakis. 2016. Non-lexical lifetimes: Introduction. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2016\/04\/27\/non-lexical-lifetimes-introduction\/  Nicholas D. Matsakis. 2016. Non-lexical lifetimes: Introduction. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2016\/04\/27\/non-lexical-lifetimes-introduction\/"},{"key":"e_1_2_2_24_1","unstructured":"Nicholas D. Matsakis. 2018. An alias-based formulation of the borrow checker. https:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/04\/27\/an-alias-based-formulation-of-the-borrow-checker\/ Blog post.  Nicholas D. Matsakis. 2018. An alias-based formulation of the borrow checker. https:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/04\/27\/an-alias-based-formulation-of-the-borrow-checker\/ Blog post."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004154"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_28_1","unstructured":"Jim Peters. 2019. The QCell library. https:\/\/crates.io\/crates\/qcell  Jim Peters. 2019. The QCell library. https:\/\/crates.io\/crates\/qcell"},{"key":"e_1_2_2_29_1","unstructured":"petgraph. 2021. petgraph. https:\/\/crates.io\/crates\/petgraph  petgraph. 2021. petgraph. https:\/\/crates.io\/crates\/petgraph"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_2_2_32_1","volume-title":"Matsakis","author":"Stone Josh","year":"2017"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"key":"e_1_2_2_35_1","unstructured":"Joshua Yanovski Hoang-Hai Dang Ralf Jung and Derek Dreyer. 2021. Coq development and supplementary material accompanying this paper. https:\/\/plv.mpi-sws.org\/rustbelt\/ghostcell\/  Joshua Yanovski Hoang-Hai Dang Ralf Jung and Derek Dreyer. 2021. Coq development and supplementary material accompanying this paper. https:\/\/plv.mpi-sws.org\/rustbelt\/ghostcell\/"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473597","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473597","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473597"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":34,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473597"],"URL":"https:\/\/doi.org\/10.1145\/3473597","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}