{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:51:23Z","timestamp":1787068283790,"version":"3.56.0"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"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":[[2026,1,8]]},"abstract":"<jats:p>Disentanglement is a runtime property of parallel programs guaranteeing that parallel tasks remain oblivious to each other\u2019s allocations. As demonstrated in the MaPLe compiler and run-time system, disentanglement can be exploited for fast automatic memory management, especially task-local garbage collection with no synchronization between parallel tasks. However, as a low-level property, disentanglement can be difficult to reason about for programmers. The only means of statically verifying disentanglement so far has been DisLog, an Iris-fueled variant of separation logic, mechanized in the Rocq proof assistant. DisLog is a fully-featured program logic, allowing for proof of functional correctness as well as verification of disentanglement. Yet its employment requires significant expertise and per-program proof effort.<\/jats:p>\n                  <jats:p>\n                    This paper explores the route of automatic verification via a type system, ensuring that any well-typed program is disentangled and lifting the burden of carrying out manual proofs from the programmer. It contributes TypeDis, a type system inspired by region types, where each type is annotated with a timestamp, identifying the task that allocated it. TypeDis supports iso-recursive types as well as polymorphism over both types and timestamps. Crucially, timestamps are allowed to change during type-checking, at join points as well as via a form of subtyping, dubbed\n                    <jats:italic toggle=\"yes\">subtiming<\/jats:italic>\n                    . The paper illustrates TypeDis and its features on a range of examples. The soundness of TypeDis and the examples are mechanized in the Rocq proof assistant, using an improved version of DisLog, dubbed DisLog2.\n                  <\/jats:p>","DOI":"10.1145\/3776655","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"354-383","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["TypeDis: A Type System for Disentanglement"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2169-1977","authenticated-orcid":false,"given":"Alexandre","family":"Moine","sequence":"first","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8347-3529","authenticated-orcid":false,"given":"Stephanie","family":"Balzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6455-9217","authenticated-orcid":false,"given":"Alex","family":"Xu","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2848-9808","authenticated-orcid":false,"given":"Sam","family":"Westrick","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3626183.3659966"},{"key":"e_1_3_2_3_1","unstructured":"Umut A. Acar Jatin Arora Matthew Fluet Ram Raghunathan Sam Westrick and Rohan Yadav. 2020. MPL: A high-performance compiler for Parallel ML. https:\/\/github.com\/MPLLang\/mpl"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SNAPL.2015.1"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","unstructured":"Umut A. Acar Arthur Chargu\u00e9raud Mike Rainey and Filip Sieczkowski. 2016. Dag-calculus: a calculus for parallel computation. In International Conference on Functional Programming (ICFP). 18\u201332. https:\/\/doi.org\/10.1145\/2951913.2951946 10.1145\/2951913.2951946","DOI":"10.1145\/2951913.2951946"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508422"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/129099"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632895"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434299"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591284"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_3_2_12_1","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"Barendregt Henk P.","year":"1984","unstructured":"Henk P. Barendregt. 1984. The Lambda Calculus, Its Syntax and Semantics. Elsevier. http:\/\/www.elsevier.com\/wps\/find\/bookdescription.cws_home\/501727\/description"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582440"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604156"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/504282.504287"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2019.39"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_2_19_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall. http:\/\/dl.acm.org\/citation.cfm?id=10510"},{"key":"e_1_3_2_20_1","volume-title":"Proof of Programs with Effect Handlers","author":"Vilhena Paulo Em\u00edlio de","year":"2022","unstructured":"Paulo Em\u00edlio de Vilhena. 2022. Proof of Programs with Effect Handlers. Theses. Universit\u00e9 Paris Cit\u00e9. https:\/\/inria.hal.science\/tel-03891381"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470654"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2024.11"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.5381\/JOT.2005.4.8.A1"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591256"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704859"},{"key":"e_1_3_2_27_1","volume-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur","author":"Girard Jean-Yves","year":"1972","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se d\u2019\u00c9tat. Universit\u00e9 Paris 7. https:\/\/girard.perso.math.cnrs.fr\/These.pdf"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178494"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_33_1","unstructured":"Steve Klabnik and Carol Nichols. 2023. The Rust programming language. No Starch Press."},{"key":"e_1_3_2_34_1","volume-title":"The Art of Computer Programming, Volume 3: (2nd Ed.) Sorting and Searching","author":"Knuth Donald E.","year":"1998","unstructured":"Donald E. Knuth. 1998. The Art of Computer Programming, Volume 3: (2nd Ed.) Sorting and Searching. Addison Wesley Longman Publishing Co., Inc., USA."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674642"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523443"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Alexandre Moine Stephanie Balzer Alex Xu and Sam Westrick. 2025a. TypeDis: A Type System for Disentanglement (Artifact). doi:10.5281\/zenodo.17336385","DOI":"10.5281\/zenodo.17336385"},{"key":"e_1_3_2_41_1","unstructured":"Alexandre Moine Stephanie Balzer Alex Xu and Sam Westrick. 2025b. TypeDis: A Type System for Disentanglement (Extended Version). (Nov. 2025). https:\/\/arxiv.org\/abs\/2511.23358"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632853"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45651-1"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062370"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0054091"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_48_1","unstructured":"Andrew M. Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. Higher Order Operational Techniques in Semantics (HOOTS) (1998) 227\u2013273."},{"key":"e_1_3_2_49_1","volume-title":"Lambda-definability and logical relations","author":"Plotkin Gordon D.","year":"1973","unstructured":"Gordon D. Plotkin. 1973. Lambda-definability and logical relations. Technical Report. University of Edinburgh."},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596983"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951935"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2312005.2312018"},{"key":"e_1_3_2_54_1","unstructured":"Vincent Simonet. 2003. Flow Caml in a Nutshell. In 1st APPSEM-II Workshop Graham Hutton (Ed.)."},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268975"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291894"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_3_2_62_1","unstructured":"VerifyThis. 2022. Challenge 3 - The World\u2019s Simplest Lock-Free Hash Set. https:\/\/ethz.ch\/content\/dam\/ethz\/special-interest\/infk\/chair-program-method\/pm\/documents\/Verify%20This\/Challenges2022\/verifyThis2022-challenge3.pdf"},{"key":"e_1_3_2_63_1","doi-asserted-by":"crossref","unstructured":"Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael-Scott queue. In Certified Programs and Proofs (CPP). 76\u201390. https:\/\/cs.au.dk\/~birke\/papers\/2021-ms-queue-final.pdf","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-42-304"},{"key":"e_1_3_2_65_1","first-page":"561","volume-title":"IFIP Working Group 2.2, 2.3 on Programming Concepts and Methods","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear Types Can Change the World!. In IFIP Working Group 2.2, 2.3 on Programming Concepts and Methods. North-Holland, 561."},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_3_2_67_1","volume-title":"Efficient and Scalable Parallel Functional Programming through Disentanglement","author":"Westrick Sam","year":"2022","unstructured":"Sam Westrick. 2022. Efficient and Scalable Parallel Functional Programming through Disentanglement. Ph. D. Dissertation. Department of Computer Science, Carnegie Mellon University."},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547646"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371115"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776655","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:39:40Z","timestamp":1784209180000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776655"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":69,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776655"],"URL":"https:\/\/doi.org\/10.1145\/3776655","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}