{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:50:17Z","timestamp":1790927417892,"version":"4.1.0"},"reference-count":37,"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":"FNSNF","award":["TMAG-2_209506\\\/1"],"award-info":[{"award-number":["TMAG-2_209506\\\/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>\n            Data races have long been a notorious problem in concurrent programming. They are hard to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress has been made in this area, and these type systems are increasingly usable and practical. However, their adoption in mainstream programming languages is still limited, which is largely attributed to their strict alias prevention principles that obstruct the usage of existing programming patterns. This is a deterrent to the migration of existing code bases. To tackle this problem, we propose Capture Separation Calculus (System CSC), a calculus that models fork-join parallelism and statically prevents data races while being compatible with established programming patterns. It follows a\n            <jats:italic>control-as-you-need<\/jats:italic>\n            philosophy: by default, aliases are allowed, but they are tracked in the type system. When data races are a concern, the tracked aliases are controlled to prevent data-race-prone patterns. We study the formal properties of System CSC. Type soundness is proven via the standard progress and preservation theorems. Additionally, we formally verify the data race freedom property of System CSC by proving that the reduction of a well-typed program is confluent.\n          <\/jats:p>","DOI":"10.1145\/3649853","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"1181-1207","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Degrees of Separation: A Flexible Type System for Safe Concurrency"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2089-6767","authenticated-orcid":false,"given":"Yichen","family":"Xu","sequence":"first","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5769-6684","authenticated-orcid":false,"given":"Aleksander","family":"Boruch-Gruszecki","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3923-8993","authenticated-orcid":false,"given":"Martin","family":"Odersky","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Nada Amin Samuel Gr\u00fctter Martin Odersky Tiark Rompf and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World.","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_2_2_4_1","volume-title":"Rinard","author":"Boyapati Chandrasekhar","year":"2001","unstructured":"Chandrasekhar Boyapati and Martin C. Rinard. 2001. A Parameterized Type System for Race-Free Java Programs. In OOPSLA. 56\u201369."},{"key":"e_1_2_2_5_1","volume-title":"Alias burying: Unique variables without destructive reads. Software: Practice and Experience, 31","author":"Boyland John Tang","year":"2001","unstructured":"John Tang Boyland. 2001. Alias burying: Unique variables without destructive reads. Software: Practice and Experience, 31 (2001)."},{"key":"e_1_2_2_6_1","article-title":"Semantics of fractional permissions with nesting","volume":"32","author":"Boyland John Tang","year":"2010","unstructured":"John Tang Boyland. 2010. Semantics of fractional permissions with nesting. ACM Trans. Program. Lang. Syst., 32 (2010), 22:1\u201322:33.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_2_8_1","volume-title":"Reference Capabilities for Concurrency Control. In European Conference on Object-Oriented Programming.","author":"Castegren Elias","year":"2016","unstructured":"Elias Castegren and Tobias Wrigstad. 2016. Reference Capabilities for Concurrency Control. In European Conference on Object-Oriented Programming."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"e_1_2_2_10_1","volume-title":"External Uniqueness Is Unique Enough. In European Conference on Object-Oriented Programming.","author":"Clarke Dave","year":"2003","unstructured":"Dave Clarke and Tobias Wrigstad. 2003. External Uniqueness Is Unique Enough. In European Conference on Object-Oriented Programming."},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"David G. Clarke John Potter and James Noble. 1998. Ownership Types for Flexible Alias Protection. In OOPSLA. 48\u201364.","DOI":"10.1145\/286942.286947"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_2_2_13_1","volume-title":"ACM-SIGACT Symposium on Principles of Programming Languages.","author":"Crary Karl","year":"1999","unstructured":"Karl Crary, David Walker, and Greg Morrisett. 1999. Typed memory management in a calculus of capabilities. In ACM-SIGACT Symposium on Principles of Programming Languages."},{"key":"e_1_2_2_14_1","volume-title":"ACM-SIGPLAN Symposium on Programming Language Design and Implementation.","author":"F\u00e4hndrich Manuel","year":"2002","unstructured":"Manuel F\u00e4hndrich and Robert A Deline. 2002. Adoption and focus: practical linear types for imperative programming. In ACM-SIGPLAN Symposium on Programming Language Design and Implementation."},{"key":"e_1_2_2_15_1","volume-title":"The Usability of Advanced Type Systems: Rust as a Case Study. ArXiv, abs\/2301.02308","author":"Ferdowsi Kasra","year":"2023","unstructured":"Kasra Ferdowsi. 2023. The Usability of Advanced Type Systems: Rust as a Case Study. ArXiv, abs\/2301.02308 (2023)."},{"key":"e_1_2_2_16_1","volume-title":"Deep Learning","author":"Goodfellow Ian","year":"2035","unstructured":"Ian Goodfellow, Yoshua Bengio, and Aaron Courville. 2016. Deep Learning. The MIT Press. isbn:0262035618"},{"key":"e_1_2_2_17_1","doi-asserted-by":"crossref","unstructured":"Colin S. Gordon Matthew J. Parkinson Jared Parsons Aleks Bromfield and Joe Duffy. 2012. Uniqueness and Reference Immutability for Safe Parallelism. In OOPSLA. 21\u201340.","DOI":"10.1145\/2398857.2384619"},{"key":"e_1_2_2_18_1","volume-title":"Conference on Object-Oriented Programming Systems, Languages, and Applications.","author":"Hogg J.","year":"1991","unstructured":"J. Hogg. 1991. Islands: aliasing protection in object-oriented languages. In Conference on Object-Oriented Programming Systems, Languages, and Applications."},{"key":"e_1_2_2_19_1","volume-title":"The Rust Programming Language","author":"Klabnik Steve","unstructured":"Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press, USA. isbn:1593278284"},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages.","author":"Leijen Daan","year":"2017","unstructured":"Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2818302.2818306"},{"key":"e_1_2_2_22_1","volume-title":"Linearity and Uniqueness: An Entente Cordiale. In European Symposium on Programming.","author":"Marshall Daniel","unstructured":"Daniel Marshall, Michael Vollmer, and Dominic A. Orchard. 2022. Linearity and Uniqueness: An Entente Cordiale. In European Symposium on Programming."},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation.","author":"Milano Mae","unstructured":"Mae Milano, Joshua Turcotti, and Andrew C. Myers. 2022. A flexible type system for fearless concurrency. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation."},{"key":"e_1_2_2_24_1","volume-title":"Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. USA. AAI3245526","author":"Miller Mark Samuel","year":"2006","unstructured":"Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. USA. AAI3245526"},{"key":"e_1_2_2_25_1","volume-title":"Rusty Links in Local Chains. ArXiv, abs\/2205.00795","author":"Noble James","year":"2022","unstructured":"James Noble, Julian Mackay, and Tobias Wrigstad. 2022. Rusty Links in Local Chains. ArXiv, abs\/2205.00795 (2022)."},{"key":"e_1_2_2_26_1","volume-title":"Observers for Linear Types. In European Symposium on Programming.","author":"Odersky Martin","year":"1992","unstructured":"Martin Odersky. 1992. Observers for Linear Types. In European Symposium on Programming."},{"key":"e_1_2_2_27_1","volume-title":"Jonathan Immanuel Brachth\u00e4user, and Ondrej Lhot\u00e1k","author":"Odersky Martin","year":"2022","unstructured":"Martin Odersky, Aleksander Boruch-Gruszecki, Edward Lee, Jonathan Immanuel Brachth\u00e4user, and Ondrej Lhot\u00e1k. 2022. Scoped Capabilities for Polymorphic Effects. ArXiv, abs\/2207.03402 (2022)."},{"key":"e_1_2_2_28_1","volume-title":"Robert D. Tennent, and Makoto Takeyama.","author":"O\u2019Hearn Peter W.","year":"1999","unstructured":"Peter W. O\u2019Hearn, John Power, Robert D. Tennent, and Makoto Takeyama. 1999. Syntactic control of interference revisited. In Mathematical Foundations of Programming Semantics."},{"key":"e_1_2_2_29_1","first-page":"1","article-title":"Implementation Strategies for Mutable Value Semantics","volume":"21","author":"Racordon Dimitri","year":"2022","unstructured":"Dimitri Racordon, Denys Shabalin, Daniel Zheng, Dave Abrahams, and Brennan Saeta. 2022. Implementation Strategies for Mutable Value Semantics. J. Object Technol., 21 (2022), 2:1\u201311.","journal-title":"J. Object Technol."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360571"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766"},{"key":"e_1_2_2_32_1","unstructured":"Scala. 2022. The Scala 3 compiler also known as Dotty. https:\/\/dotty.epfl.ch"},{"key":"e_1_2_2_33_1","unstructured":"Marco Servetto David J. Pearce Lindsay J. Groves and Alex Potanin. 2013. Balloon Types for Safe Parallelisation over Arbitrary Object Graphs."},{"key":"e_1_2_2_34_1","unstructured":"Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods."},{"key":"e_1_2_2_35_1","volume-title":"Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. ArXiv, abs\/2307.13844","author":"Wei Guannan","year":"2023","unstructured":"Guannan Wei, Oliver Bracevac, Songlin Jia, Yuyan Bao, and Tiark Rompf. 2023. Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. ArXiv, abs\/2307.13844 (2023)."},{"key":"e_1_2_2_36_1","volume-title":"Ahmed","author":"Weiss Aaron","year":"2019","unstructured":"Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal J. Ahmed. 2019. Oxide: The Essence of Rust. ArXiv, abs\/1903.00982 (2019)."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649853","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649853","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\/3649853"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":37,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649853"],"URL":"https:\/\/doi.org\/10.1145\/3649853","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"}}]}}