{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:39Z","timestamp":1780994739595,"version":"3.54.1"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            Fueled by the success of Rust, many programming languages are adding substructural features to their type systems. The promise of tracking properties such as lifetimes and sharing is tremendous, not just for low-level memory management, but also for controlling higher-level resources and capabilities. But so are the difficulties in adapting successful techniques from Rust to higher-level languages, where they need to interact with other advanced features, especially various flavors of functional and type-level abstraction. What would it take to bring full-fidelity reasoning about lifetimes and sharing to mainstream languages? Reachability types are a recent proposal that has shown promise in scaling to higher-order but monomorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. However, naive extensions on top of the prior reachability type system\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msup>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mo>*<\/mml:mo>\n                <\/mml:msup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            with type polymorphism and\/or precise reachability polymorphism are unsound, making\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msup>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mo>*<\/mml:mo>\n                <\/mml:msup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            unsuitable for adoption in real languages. Combining reachability and type polymorphism that is precise, sound, and parametric remains an open challenge.\n          <\/jats:p>\n          <jats:p>\n            This paper presents a rethinking of the design of reachability tracking and proposes new polymorphic reachability type systems. We introduce a new freshness qualifier to indicate variables whose reachability sets may grow during evaluation steps. The new system tracks variables reachable in a single step and computes transitive closures only when necessary, thus preserving chains of reachability over known variables that can be refined using substitution. These ideas yield the simply-typed\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msup>\n                  <mml:mi>\u03bb<\/mml:mi>\n                  <mml:mo>\u25c6<\/mml:mo>\n                <\/mml:msup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -calculus with precise lightweight,\n            <jats:italic toggle=\"yes\">i.e.<\/jats:italic>\n            , quantifier-free, reachability polymorphism, and the\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:msubsup>\n                  <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                  <mml:mrow>\n                    <mml:mo>&lt;<\/mml:mo>\n                    <mml:mo>:<\/mml:mo>\n                  <\/mml:mrow>\n                  <mml:mo>\u25c6<\/mml:mo>\n                <\/mml:msubsup>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -calculus with bounded parametric polymorphism over types and reachability qualifiers, paving the way for making true tracking of lifetimes and sharing practical for mainstream languages. We prove type soundness and the preservation of separation property in Coq. We discuss various applications (\n            <jats:italic toggle=\"yes\">e.g.<\/jats:italic>\n            , safe capability programming), possible effect system extensions, and compare our system with Scala\u2019s capture types.\n          <\/jats:p>","DOI":"10.1145\/3632856","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"393-424","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3150-2033","authenticated-orcid":false,"given":"Guannan","family":"Wei","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, 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":"Galois, Portland, United States"},{"name":"Purdue University, West Lafayette, 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-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":[[2024,1,5]]},"reference":[{"issue":"4","key":"e_1_3_1_2_1","first-page":"397","article-title":"A Linear Language with Locations","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundam. Informaticae 77, 4 (2007), 397\u2013449.","journal-title":"Fundam. Informaticae"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639950.1640073"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"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","DOI":"10.1145\/2837022"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_1_10_1","unstructured":"Aleksander Boruch-Gruszecki Jonathan Immanuel Brachth\u00e4user Edward Lee Ondrej Lhot\u00e1k and Martin Odersky. 2021. Tracking Captured Variables in Types. CoRR abs\/2105.11896 (2021)."},{"key":"e_1_3_1_11_1","doi-asserted-by":"crossref","unstructured":"Aleksander Boruch-Gruszecki Martin Odersky Edward Lee Ondrej Lhot\u00e1k and Jonathan Brachth\u00e4user. 2023. Capturing Types. ACM Trans. Program. Lang. Syst. (sep 2023). Just Accepted.","DOI":"10.1145\/3618003"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582440"},{"key":"e_1_3_1_13_1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"Boyland John","year":"2003","unstructured":"John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 55\u201372."},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527320"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622813"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_10"},{"key":"e_1_3_1_18_1","volume-title":"Existential Types for Variance - Java Wildcards and Ownership Types","author":"Cameron Nicholas Robert","year":"2009","unstructured":"Nicholas Robert Cameron. 2009. Existential Types for Variance - Java Wildcards and Ownership Types. Ph. D. Dissertation. Imperial College London, UK."},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1037740"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_4"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2554511.2554516"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_1_24_1","volume-title":"ICOOOLPS\u20192015","author":"Clebsch Sylvan","year":"2015","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_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007159"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001134"},{"key":"e_1_3_1_27_1","first-page":"181","volume-title":"IFL (Lecture Notes in Computer Science, Vol. 4449)","author":"Vries Edsko de","year":"2006","unstructured":"Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson. 2006. Uniqueness Typing Redefined. In IFL (Lecture Notes in Computer Science, Vol. 4449). Springer, 181\u2013198."},{"key":"e_1_3_1_28_1","first-page":"201","volume-title":"IFL (Lecture Notes in Computer Science, Vol. 5083)","author":"Vries Edsko de","year":"2007","unstructured":"Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson. 2007. Uniqueness Typing Simplified. In IFL (Lecture Notes in Computer Science, Vol. 5083). Springer, 201\u2013218."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049709"},{"issue":"5","key":"e_1_3_1_30_1","first-page":"98:1","article-title":"Bidirectional Typing","volume":"54","author":"and JanaDunfield","year":"2022","unstructured":"JanaDunfield and Neel Krishnaswami. 2022. Bidirectional Typing. ACM Comput. Surv. 54, 5 (2022), 98:1\u201398:38.","journal-title":"ACM Comput. Surv."},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"e_1_3_1_32_1","unstructured":"Colin S. Gordon. 2020. Designing with Static Capabilities and Effects: Use Mention and Invariants (Pearl). In ECOOP (LIPIcs Vol. 166). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 10:1\u201310:25."},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/117954.117975"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3549483"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_38_1","doi-asserted-by":"crossref","unstructured":"Oleg Kiselyov Yukiyoshi Kameyama and Yuto Sudo. 2016. Refined Environment Classifiers - Type- and Scope-Safe Code Generation with Mutable Cells. In APLAS (Lecture Notes in Computer Science Vol. 10017). 271\u2013291.","DOI":"10.1007\/978-3-319-47958-3_15"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_13"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_1_41_1","unstructured":"Peter M\u00fcller and Arnd Poetzsch-Heffter. 2000. A type system for controlling representation exposure in Java. In ECOOP Workshop on Formal Techniques for Java Programs."},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054091"},{"key":"e_1_3_1_45_1","unstructured":"Martin Odersky et al. 2023. Scala 3 Reference - Capture Checking. https:\/\/docs.scala-lang.org\/scala3\/reference\/experimental\/cc.html"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486610.3486893"},{"key":"e_1_3_1_47_1","unstructured":"Martin Odersky Aleksander Boruch-Gruszecki Edward Lee Jonathan Immanuel Brachth\u00e4user and Ondrej Lhot\u00e1k. 2022. Scoped Capabilities for Polymorphic Effects. CoRR abs\/2207.03402 (2022)."},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360207"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004495"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00359-4"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984009"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158101"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143228"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167500"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766"},{"key":"e_1_3_1_59_1","unstructured":"John C. Reynolds. 1988. Preliminary design of the programming language Forsythe. Tech Report CMU-CS-88-159 Carnegie Mellon University (1988)."},{"key":"e_1_3_1_60_1","first-page":"704","volume-title":"ICALP (Lecture Notes in Computer Science, Vol. 372)","author":"Reynolds John C.","year":"1989","unstructured":"John C. Reynolds. 1989. Syntactic Control of Inference, Part 2. In ICALP (Lecture Notes in Computer Science, Vol. 372). Springer, 704\u2013722."},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_47"},{"key":"e_1_3_1_64_1","unstructured":"Jeremy G. Siek Michael M. Vitousek and Jonathan D. Turner. 2012. Effects for Funargs. CoRR abs\/1201.0023 (2012)."},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_24"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_3_1_67_1","first-page":"561","volume-title":"Programming Concepts and Methods","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods. North-Holland, 561."},{"key":"e_1_3_1_68_1","unstructured":"Guannan Wei Oliver Bracevac Songlin Jia Yuyan Bao and Tiark Rompf. 2023. Polymorphic Reachability Types: Tracking Freshness Aliasing and Separation in Higher-Order Generic Programs (Extended Version). CoRR abs\/2307.13844 (2023)."},{"key":"e_1_3_1_69_1","first-page":"15:1","volume-title":"ECOOP (LIPIcs, Vol. 222)","author":"Xhebraj Anxhelo","year":"2022","unstructured":"Anxhelo Xhebraj, Oliver Bracevac, Guannan Wei, and Tiark Rompf. 2022. What If We Don\u2019t Pop the Stack? The Return of 2nd-Class Values. In ECOOP (LIPIcs, Vol. 222). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 15:1\u201315:29."},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.04.001"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571241"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3549537"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632856","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632856","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632856","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:03:51Z","timestamp":1751659431000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632856"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":71,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632856"],"URL":"https:\/\/doi.org\/10.1145\/3632856","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}