{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:43Z","timestamp":1780994743945,"version":"3.54.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"NSF","award":["2348334"],"award-info":[{"award-number":["2348334"]}]}],"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>Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages, with a focus on higher-order functions, parametric types, and shared mutable state -- features that are only partially supported by current  \ntechniques as employed in Rust. While prior work has established key type soundness results for reachability types using the usual  \nsyntactic techniques of progress and preservation, stronger metatheoretic properties have so far been unexplored. This paper presents an alternative semantic model of reachability types using logical relations, providing a framework  \nin which we study key properties of interest: (1) semantic type soundness, including of not syntactically well-typed code fragments,  \n(2) termination, especially in the presence of higher-order mutable references, (3) effect safety, especially the absence of observable mutation, and, finally, (4) program equivalence, especially reordering of non-interfering expressions for parallelization or compiler optimization.<\/jats:p>","DOI":"10.1145\/3763116","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1837-1864","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3832-3134","authenticated-orcid":false,"given":"Yuyan","family":"Bao","sequence":"first","affiliation":[{"name":"Augusta University, Augusta, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2526-0438","authenticated-orcid":false,"given":"Songlin","family":"Jia","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3150-2033","authenticated-orcid":false,"given":"Guannan","family":"Wei","sequence":"additional","affiliation":[{"name":"Tufts University, Medford and Somerville, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3569-4869","authenticated-orcid":false,"given":"Oliver","family":"Bra\u010devac","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2068-3238","authenticated-orcid":false,"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Amal Ahmed Derek Dreyer and Andreas Rossberg. 2009. State-dependent representation independence. In POPL. ACM 340\u2013353. https:\/\/doi.org\/10.1145\/1480881.1480925 10.1145\/1480881.1480925","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_1_2_1","volume-title":"Semantics of types for mutable state","author":"Ahmed Amal Jamil","unstructured":"Amal Jamil Ahmed. 2004. Semantics of types for mutable state. Princeton University."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"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","unstructured":"Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM 666\u2013679. https:\/\/doi.org\/10.1145\/3009837.3009866 10.1145\/3009837.3009866","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Yuyan Bao. 2025. Reproduction Package for Article \u2019Modeling Reachability Types with Logical Relations\u2019. https:\/\/doi.org\/10.5281\/zenodo.16934167 10.5281\/zenodo.16934167","DOI":"10.5281\/zenodo.16934167"},{"key":"e_1_2_1_8_1","unstructured":"Yuyan Bao Songlin Jia Guannan Wei Oliver Bra\u010devac and Tiark Rompf. 2025. Modeling Reachability Types with Logical Relations: Semantic Type Soundness Termination and Equational Theory (Extended Version). arxiv:2309.05885."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Nick Benton Martin Hofmann and Vivek Nigam. 2014. Abstract effects and proof-relevant logical relations. In POPL. ACM 619\u2013632. https:\/\/doi.org\/10.1145\/2535838.2535869 10.1145\/2535838.2535869","DOI":"10.1145\/2535838.2535869"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Nick Benton Martin Hofmann and Vivek Nigam. 2016. Effect-dependent transformations for concurrent programs. In PPDP. ACM 188\u2013201. https:\/\/doi.org\/10.1145\/2967973.2968602 10.1145\/2967973.2968602","DOI":"10.1145\/2967973.2968602"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Nick Benton Andrew Kennedy Lennart Beringer and Martin Hofmann. 2007. Relational semantics for effect-based program transformations with dynamic allocation. In PPDP. ACM 87\u201396. https:\/\/doi.org\/10.1145\/1273920.1273932 10.1145\/1273920.1273932","DOI":"10.1145\/1273920.1273932"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Nick Benton Andrew Kennedy Lennart Beringer and Martin Hofmann. 2009. Relational semantics for effect-based program transformations: higher-order store. In PPDP. ACM 301\u2013312. https:\/\/doi.org\/10.1145\/1599410.1599447 10.1145\/1599410.1599447","DOI":"10.1145\/1599410.1599447"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_7"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563319"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2016.04.003"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_2"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622813"},{"key":"e_1_2_1_20_1","unstructured":"Oliver Bra\u010devac Guannan Wei Songlin Jia Supun Abeysinghe Yuxuan Jiang Yuyan Bao and Tiark Rompf. 2023. Graph IRs for Impure Higher-Order Languages (Supplement). arxiv:2309.08118."},{"key":"e_1_2_1_21_1","volume-title":"40th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS","author":"Bunting B","year":"2025","unstructured":"B Bunting and AS Murawski. 2025. Reachability types, traces and full abstraction. 40th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2025), https:\/\/ora.ox.ac.uk\/objects\/uuid:7ec96a90-1bb8-408d-90a8-26126a3bbc05"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2016.5"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"David Clarke John Potter and James Noble. 1998. Ownership Types for Flexible Alias Protection. In OOPSLA. ACM 48\u201364.","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_25_1","volume-title":"\u2019Pony\u2019: co-designing a type system and a runtime. Ph. D. Dissertation","author":"Clebsch Sylvan","unstructured":"Sylvan Clebsch. 2017. \u2019Pony\u2019: co-designing a type system and a runtime. Ph. D. Dissertation. Imperial College London, UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.769552"},{"key":"e_1_2_1_26_1","unstructured":"Sylvan Clebsch Sebastian Blessing Juliana Franco and Sophia Drossopoulou. 2015. Ownership and reference counting based garbage collection in the actor world. In ICOOOLPS\u20192015. ACM."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Sylvan Clebsch Sophia Drossopoulou Sebastian Blessing and Andy McNeil. 2015. Deny capabilities for safe fast actors. In AGERE SPLASH. ACM 1\u201312. https:\/\/doi.org\/10.1145\/2824815.2824816 10.1145\/2824815.2824816","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763172"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_1_30_1","unstructured":"Sophia Drossopoulou Julian Mackay Susan Eisenbach and James Noble. 2025. Reasoning about External Calls. arxiv:2506.06544."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111062"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2018.11.007"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2018.09.001"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Colin S. Gordon Matthew J. Parkinson Jared Parsons Aleks Bromfield and Joe Duffy. 2012. Uniqueness and reference immutability for safe parallelism. In OOPSLA. ACM 21\u201340. https:\/\/doi.org\/10.1145\/2384616.2384619 10.1145\/2384616.2384619","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_17"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/117954.117975"},{"key":"e_1_2_1_37_1","unstructured":"Songlin Jia Guannan Wei Siyuan He Yueyang Tang Yuyan Bao and Tiark Rompf. 2024. Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking. arxiv:2404.08217."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. ACM 256\u2013269. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1093\/COMJNL\/6.4.308"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649848"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Karl Naden Robert Bocchino Jonathan Aldrich and Kevin Bierhoff. 2012. A type system for borrowing permissions. In POPL. ACM 557\u2013570. https:\/\/doi.org\/10.1145\/2103656.2103722 10.1145\/2103656.2103722","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054091"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_1_50_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press. isbn:0262162288"},{"key":"e_1_2_1_51_1","volume-title":"Lambda Definability and Logical Relations","author":"Plotkin G. D.","year":"1973","unstructured":"G. D. Plotkin. 1973. Lambda Definability and Logical Relations. University of Edinburgh. https:\/\/homepages.inf.ed.ac.uk\/gdp\/publications\/logical_relations_1973.pdf"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","unstructured":"Alex Potanin James Noble Dave Clarke and Robert Biddle. 2006. Generic ownership for generic Java. In OOPSLA. ACM 311\u2013324. https:\/\/doi.org\/10.1145\/1167473.1167500 10.1145\/1167473.1167500","DOI":"10.1145\/1167473.1167500"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In OOPSLA. ACM 624\u2013641. https:\/\/doi.org\/10.1145\/2983990.2984008 10.1145\/2983990.2984008","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_2_1_55_1","unstructured":"Jeremy Siek. 2013. Type safety in three easy lemmas. http:\/\/siek.blogspot.com\/2013\/05\/type-safety-in-three-easy-lemmas.html"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Jacob Thamsborg and Lars Birkedal. 2011. A Kripke logical relation for effect-based program transformations. In ICFP. ACM 445\u2013456. https:\/\/doi.org\/10.1145\/2034773.2034831 10.1145\/2034773.2034831","DOI":"10.1145\/2034773.2034831"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.27"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1994.1093"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","unstructured":"Yichen Xu 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"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:47:12Z","timestamp":1760032032000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":64,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763116"],"URL":"https:\/\/doi.org\/10.1145\/3763116","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","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"}}]}}