{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:00:16Z","timestamp":1784239216349,"version":"3.55.0"},"reference-count":64,"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":[{"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 techniques as employed in Rust. While prior work has established key type soundness results for reachability types using the usual syntactic 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 in which we study key properties of interest: (1) semantic type soundness, including of not syntactically well-typed code fragments, (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":5,"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_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1037736"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM 666\u2013679. doi:10.1145\/3009837.3009866","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Yuyan Bao. 2025. Reproduction Package for Article 'Modeling Reachability Types with Logical Relations'. doi:10.5281\/zenodo.16934167","DOI":"10.5281\/zenodo.16934167"},{"key":"e_1_3_1_9_1","doi-asserted-by":"crossref","unstructured":"Yuyan Bao Songlin Jia Guannan Wei liver Bra\u010devac and Tiark Rompf. 2025. Modeling Reachability Types with Logical Relations: Semantic Type Soundness Termination and Equational Theory (Extended Version). arXiv:2309.05885 [cs.PL]","DOI":"10.1145\/3763116"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535869"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968602"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273932"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599447"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_7"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563319"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Guilhem Jaber Filip Sieczkowski and Jacob Thamsborg. 2016. A Kripke logical relation for effect-based program transformations. Inf. Comput. 249 (2016) 160\u2013189. doi:10.1016\/J.IC.2016.04.003","DOI":"10.1016\/J.IC.2016.04.003"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_2"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622813"},{"key":"e_1_3_1_21_1","unstructured":"Oliver Bra\u010devac Guannan Wei Songlin Jia Supun Abeysinghe Yuxuan Jiang Yuyan Bao and Tiark Rompf. 2023b. Graph IRs for Impure Higher-Order Languages (Supplement). arXiv:2309.08118 [cs.PL]"},{"key":"e_1_3_1_22_1","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) (2025). https:\/\/ora.ox.ac.uk\/objects\/uuid:7ec96a90-1bb8-408d-90a8-26126a3bbc05 https:\/\/ora.ox.ac.uk\/objects\/uuid:7ec96a90-1bb8-408d-90a8-26126a3bbc05"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2016.5"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_1_26_1","volume-title":"'Pony': co-designing a type system and a runtime","author":"Clebsch Sylvan","year":"2017","unstructured":"Sylvan Clebsch. 2017. 'Pony': 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 https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.769552"},{"key":"e_1_3_1_27_1","volume-title":"In ICOOOLPS'2015.","author":"Clebsch Sylvan","year":"2015","unstructured":"Sylvan Clebsch, Sebastian Blessing, Juliana Franco, and Sophia Drossopoulou. 2015a. Ownership and reference counting based garbage collection in the actor world. In ICOOOLPS'2015. ACM."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Sylvan Clebsch Sophia Drossopoulou Sebastian Blessing and Andy McNeil. 2015b. Deny capabilities for safe fast actors. In AGERE SPLASH. ACM 1\u201312. doi:10.1145\/2824815.2824816","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763172"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_3_1_31_1","doi-asserted-by":"crossref","unstructured":"Sophia Drossopoulou Julian Mackay Susan Eisenbach and James Noble. 2025. Reasoning about External Calls. arXiv:2506.06544 [cs.PL]","DOI":"10.1145\/3763064"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111062"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Paola Giannini Tim Richter Marco Servetto and Elena Zucca. 2019a. Tracing sharing in an imperative pure calculus. Sci. Comput. Program. 172 (2019) 180\u2013202. doi:10.1016\/J.SCICO.2018.11.007","DOI":"10.1016\/J.SCICO.2018.11.007"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Paola Giannini Marco Servetto Elena Zucca and James Cone. 2019b. Flexible recovery of uniqueness and immutability. Theor. Comput. Sci. 764 (2019) 145\u2013172. doi:10.1016\/J.TCS.2018.09.001","DOI":"10.1016\/J.TCS.2018.09.001"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_17"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/117954.117975"},{"key":"e_1_3_1_38_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 [cs.PL]"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2018a. RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2 POPL (2018) 66:1\u201366:34. doi:10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. F. Funct. Program. 28 (2018) e20. doi:10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1093\/COMJNL\/6.4.308"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649848"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054091"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1104.001.0001"},{"key":"e_1_3_1_52_1","volume-title":"Memorandum SAI-RM-4","author":"Plotkin G. D.","year":"1973","unstructured":"G. D. Plotkin. 1973. Lambda Definability and Logical Relations. Memorandum SAI-RM-4. University of Edinburgh. https:\/\/homepages.inf.ed.ac.uk\/gdp\/publications\/logical_relations_1973.pdf https:\/\/homepages.inf.ed.ac.uk\/gdp\/publications\/logical_relations_1973.pdf"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167500"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_3_1_56_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_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034831"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. J. ACM 71 6 (2024) 40:1\u201340:75. doi:10.1145\/3676954","DOI":"10.1145\/3676954"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.27"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","unstructured":"Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115 1 (1994) 38\u201394. doi:10.1006\/INCO.1994.1093","DOI":"10.1006\/INCO.1994.1093"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","unstructured":"Yichen Xu and Martin Odersky. 2023. Degrees of Separation: A Flexible Type System for Data Race Prevention. doi: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":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763116","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:06:36Z","timestamp":1784196396000},"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"}}]}}