{"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":1780994743194,"version":"3.54.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"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":[[2026,6,8]]},"abstract":"<jats:p>Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its \u201cshared XOR mutable\u201d model is fundamentally at odds with higher-level functional programming. Reachability types offer an alternative: they enable safe sharing and escape of mutable data by tracking which resources each expression can reach.<\/jats:p>\n                  <jats:p>\n                    To track internal reachability within complex object graphs, reachability types adopt\n                    <jats:italic toggle=\"yes\">self-references<\/jats:italic>\n                    that let components refer to enclosing resources from inside, just like this pointers in OO languages. While natural for\n                    <jats:italic toggle=\"yes\">declaratively<\/jats:italic>\n                    typing escaping data, self-references complicate subtyping and furthermore type inference: variance restricts where self-references may appear, yet useful type conversions must allow them to vary in controlled ways, which in turn imposes constraints on inference. As an undesirable result, prior works require programmers to insert term-level coercions for even just\n                    <jats:italic toggle=\"yes\">avoidance<\/jats:italic>\n                    \u2014avoiding ill-scoped names in types.\n                  <\/jats:p>\n                  <jats:p>\n                    With all prior works being declarative, we investigate\n                    <jats:italic toggle=\"yes\">algorithmic<\/jats:italic>\n                    reachability types in this work. We introduce a refined subtyping relation that permits more flexible usages of self-references. We further develop a sound and decidable bidirectional typing algorithm, implemented and verified in Lean. The algorithm automatically avoids ill-scoped names in types, and infers qualifiers via a lightweight unification mechanism. As a step towards practical reachability programming, we show that the system is capable of tracking diverse reachability patterns without explicit coercions in complex Church-encoded datatypes.\n                  <\/jats:p>","DOI":"10.1145\/3808335","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"2204-2228","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-2526-0438","authenticated-orcid":false,"given":"Songlin","family":"Jia","sequence":"first","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, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7130-5592","authenticated-orcid":false,"given":"Siyuan","family":"He","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3832-3134","authenticated-orcid":false,"given":"Yuyan","family":"Bao","sequence":"additional","affiliation":[{"name":"Augusta University, Augusta, USA"}],"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":[[2026,6,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_1_3_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_4_1","doi-asserted-by":"publisher","unstructured":"Nada Amin and Ross Tate. 2016. Java and scala\u2019s type systems are unsound: the existential crisis of null pointers. In OOPSLA. ACM 838\u2013848. https:\/\/doi.org\/10.1145\/2983990.2984004 10.1145\/2983990.2984004","DOI":"10.1145\/2983990.2984004"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763116"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704902"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Stephan Brandauer Dave Clarke and Tobias Wrigstad. 2015. Disjointness domains for fine-grained aliasing. In OOPSLA. ACM 898\u2013916. https:\/\/doi.org\/10.1145\/2814270.2814280 10.1145\/2814270.2814280","DOI":"10.1145\/2814270.2814280"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0055784"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"David Clarke John Potter and James Noble. 1998. Ownership Types for Flexible Alias Protection. In OOPSLA. ACM 48\u201364. https:\/\/doi.org\/10.1145\/286936.286947 10.1145\/286936.286947","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622871"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763172"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2510.08939"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22655-7_16"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Stephen Dolan and Alan Mycroft. 2017. Polymorphism subtyping and type inference in MLsub. In POPL. ACM 60\u201372. https:\/\/doi.org\/10.1145\/3009837.3009882 10.1145\/3009837.3009882","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Derek Dreyer Karl Crary and Robert Harper. 2003. A type system for higher-order modules. In POPL. ACM 236\u2013249. https:\/\/doi.org\/10.1145\/604131.604151 10.1145\/604131.604151","DOI":"10.1145\/604131.604151"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Jana Dunfield and Frank Pfenning. 2004. Tridirectional typechecking. In POPL. ACM 281\u2013292. https:\/\/doi.org\/10.1145\/964001.964025 10.1145\/964001.964025","DOI":"10.1145\/964001.964025"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763144"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00037-J"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00300-3"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_9"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Songlin Jia Guannan Wei Siyuan He Yuyan Bao and Tiark Rompf. 2026. Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types (Artifact). https:\/\/doi.org\/10.5281\/zenodo.19340767 10.5281\/zenodo.19340767","DOI":"10.5281\/zenodo.19340767"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Songlin Jia Guannan Wei Siyuan He Yuyan Bao and Tiark Rompf. 2026. Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types (Extended Version). https:\/\/doi.org\/10.48550\/arXiv.2404.08217 10.48550\/arXiv.2404.08217","DOI":"10.48550\/arXiv.2404.08217"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003683"},{"key":"e_1_2_1_32_1","volume-title":"Translucent Sums: A Foundation for Higher-Order Module Systems. Ph. D. Dissertation.","author":"Lillibridge Mark","year":"1996","unstructured":"Mark Lillibridge. 1996. Translucent Sums: A Foundation for Higher-Order Module Systems. Ph. D. Dissertation."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0054091"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2207.03402"},{"key":"e_1_2_1_37_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_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Martin Odersky Christoph Zenger and Matthias Zenger. 2001. Colored local type inference. In POPL. ACM 41\u201353. https:\/\/doi.org\/10.1145\/360204.360207 10.1145\/360204.360207","DOI":"10.1145\/360204.360207"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Leo Osvald Gr\u00e9gory M. Essertel Xilun Wu Lilliam I. Gonz\u00e1lez Alay\u00f3n and Tiark Rompf. 2016. Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect. In OOPSLA. ACM 234\u2013251. https:\/\/doi.org\/10.1145\/2983990.2984009 10.1145\/2983990.2984009","DOI":"10.1145\/2983990.2984009"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Nadia Polikarpova Ivan Kuraj and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In PLDI. ACM 522\u2013538. https:\/\/doi.org\/10.1145\/2908080.2908093 10.1145\/2908080.2908093","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_1_45_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_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_47_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_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Lukas Rytz and Martin Odersky. 2012. Relative Effect Declarations for Lightweight Effect-Polymorphism. http:\/\/infoscience.epfl.ch\/record\/175546","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00354-010-0100-1"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2022.15"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649853"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3763112"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2022.2"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341716"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571241"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869509"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808335","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808335","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T19:57:13Z","timestamp":1780948633000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808335"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":60,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808335"],"URL":"https:\/\/doi.org\/10.1145\/3808335","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}