{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:20:06Z","timestamp":1760059206631,"version":"build-2065373602"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2348334"],"award-info":[{"award-number":["2348334"]}],"id":[{"id":"10.13039\/100000001","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":[[2025,10,9]]},"abstract":"<jats:p>Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches \u2013 ownership systems, linear and affine types, uniqueness types, and lexical effect tracking \u2013 impose global restrictions such as uniqueness or linearity, or rely on shallow syntactic analyses. These designs fall short with higher-order functions and shared mutable state. Reachability Types (RT) track aliasing and separation in higher-order programs, ensuring runtime safety and non-interference. However, RT systems face three key limitations: (1) they prohibit cyclic references, ruling out non-terminating computations and fixed-point combinators; (2) they require deep tracking, where a qualifier must include all transitively reachable locations, reducing precision and hindering optimizations like fine-grained parallelism; and (3) referent qualifier invariance prevents referents from escaping their allocation contexts, making reference factories inexpressible.<\/jats:p>\n          <jats:p>\n            In this work, we address these limitations by extending RT with three mechanisms that enhance expressiveness. First, we introduce cyclic references, enabling recursive patterns to be encoded directly through the store. Second, we adopt shallow qualifier tracking, decoupling references from their transitively reachable values. Finally, we introduce an escaping rule with reference subtyping, allowing referent qualifiers to outlive their allocation context. These extensions are formalized in the\n            <jats:italic toggle=\"yes\">F<\/jats:italic>\n            <jats:sub>&lt;:<\/jats:sub>\n            <jats:sup>\u2218<\/jats:sup>\n            -calculus with a mechanized proof of type soundness, and case studies illustrate expressiveness through fixpoint combinators, non-interfering parallelism, and escaping read-only references.\n          <\/jats:p>","DOI":"10.1145\/3763172","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"3398-3425","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Complete the Cycle: Reachability Types with Expressive Cyclic References"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7096-2646","authenticated-orcid":false,"given":"Haotian","family":"Deng","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7130-5592","authenticated-orcid":false,"given":"Siyuan","family":"He","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2526-0438","authenticated-orcid":false,"given":"Songlin","family":"Jia","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3832-3134","authenticated-orcid":false,"given":"Yuyan","family":"Bao","sequence":"additional","affiliation":[{"name":"Augusta University, Augusta, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2068-3238","authenticated-orcid":false,"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561324"},{"key":"e_1_2_1_2_1","first-page":"397","article-title":"L^ 3: A Linear Language with Locations","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L^ 3: A Linear Language with Locations. Fundamenta Informaticae, 77, 4 (2007), Jan., 397\u2013449. issn:0169-2968","journal-title":"Fundamenta Informaticae"},{"volume-title":"Semantics of Types for Mutable State","author":"Ahmed Amal Jamil","key":"e_1_2_1_3_1","unstructured":"Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Princeton University."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622846"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763116"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0048939"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622813"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292564"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434314"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Haotian Deng. 2025. Reproduction Package for Article \u2019Complete the Cycle: Reachability Types with Expressive Cyclic References\u2019. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.16995621 10.5281\/zenodo.16995621","DOI":"10.5281\/zenodo.16995621"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Haotian Deng Siyuan He Songlin Jia Yuyan Bao and Tiark Rompf. 2025. Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version). arxiv:2503.07328. https:\/\/doi.org\/10.48550\/arXiv.2503.07328 10.48550\/arXiv.2503.07328","DOI":"10.48550\/arXiv.2503.07328"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2020.18"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.13"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186632.1186635"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-005-4881-8"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_17"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/117954.117975"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384680"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Songlin Jia Guannan Wei Siyuan He Yuyan Bao and Tiark Rompf. 2024. Escape with Your Self: A Solution to the Avoidance Problem with Decidable Bidirectional Typing for Reachability Types. arxiv:2404.08217. https:\/\/doi.org\/10.48550\/arXiv.2404.08217 10.48550\/arXiv.2404.08217","DOI":"10.48550\/arXiv.2404.08217"},{"key":"e_1_2_1_31_1","unstructured":"Oleg Kiselyov. 2020. Many Faces of the Fixed-Point Combinator. https:\/\/okmij.org\/ftp\/Computation\/fixed-point-combinators.html."},{"key":"e_1_2_1_32_1","unstructured":"Paulette Koronkevich and William J Bowman. 2022. One Weird Trick to Untie Landin\u2019s Knot."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622828"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523443"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611096.3611097"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","key":"e_1_2_1_40_1","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press. isbn:978-0-262-16209-8"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3103111.3104036"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"volume-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers H.","key":"e_1_2_1_43_1","unstructured":"H. (Hartley) Rogers. 1967. Theory of Recursive Functions and Effective Computability. New York, McGraw-Hill."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984008"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516507.1516510"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_24"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_1_48_1","volume-title":"Programming Concepts and Methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 2-5 April, 1990, Manfred Broy and Cliff B. Jones (Eds.). North-Holland, 561."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/363911.363923"},{"volume-title":"Types in Compilation (Lecture Notes in Computer Science","author":"Walker David","key":"e_1_2_1_50_1","unstructured":"David Walker and J. Gregory Morrisett. 2000. Alias Types for Recursive Data Structures. In Types in Compilation (Lecture Notes in Computer Science, Vol. 2071). Springer, 177\u2013206."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","unstructured":"Yichen Xu Aleksander Boruch-Gruszecki and Martin Odersky. 2023. Degrees of Separation: A Flexible Type System for Data Race Prevention. https:\/\/doi.org\/10.48550\/ARXIV.2308.07474 10.48550\/ARXIV.2308.07474","DOI":"10.48550\/ARXIV.2308.07474"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649853"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763172","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763172","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:41:26Z","timestamp":1760031686000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763172"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":53,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763172"],"URL":"https:\/\/doi.org\/10.1145\/3763172","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}