{"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":1780994743139,"version":"3.54.1"},"reference-count":112,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000038","name":"NSERC","doi-asserted-by":"crossref","award":["CRDPJ 543583-19"],"award-info":[{"award-number":["CRDPJ 543583-19"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]},{"name":"DOE","award":["DE-SC0018050"],"award-info":[{"award-number":["DE-SC0018050"]}]},{"name":"NSF","award":["1553471, 1564207, 1918483, 1910216"],"award-info":[{"award-number":["1553471, 1564207, 1918483, 1910216"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>\n            Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, \u03bb\n            <jats:sup>*<\/jats:sup>\n            , which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization.\n          <\/jats:p>","DOI":"10.1145\/3485516","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Reachability types: tracking aliasing and separation in higher-order functional programs"],"prefix":"10.1145","volume":"5","author":[{"given":"Yuyan","family":"Bao","sequence":"first","affiliation":[{"name":"University of Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guannan","family":"Wei","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oliver","family":"Bra\u010devac","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuxuan","family":"Jiang","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qiyang","family":"He","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328449"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1365997.1366003"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781146"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1639950.1640073"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_14"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009866"},{"key":"e_1_2_2_7_1","unstructured":"Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics Vol. 103). North-Holland.  Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics Vol. 103). North-Holland."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290319"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_2_2_12_1","volume-title":"Edward Lee, Ond\u0159ej Lhot\u00e1k, and Martin Odersky.","author":"Boruch-Gruszecki Aleksander","year":"2021","unstructured":"Aleksander Boruch-Gruszecki , Jonathan Immanuel Brachth\u00e4user , Edward Lee, Ond\u0159ej Lhot\u00e1k, and Martin Odersky. 2021 . Tracking Captured Variables in Types . May, technical report. arxiv:2105.11896 (v1). arxiv:2105.11896 Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachth\u00e4user, Edward Lee, Ond\u0159ej Lhot\u00e1k, and Martin Odersky. 2021. Tracking Captured Variables in Types. May, technical report. arxiv:2105.11896 (v1). arxiv:2105.11896"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/583854.582440"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760273"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646158.680004"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000027"},{"key":"e_1_2_2_18_1","unstructured":"Walter Bright. 2019. Ownership and Borrowing in D. https:\/\/web.archive.org\/web\/20210105083139\/https:\/\/dlang.org\/blog\/2019\/07\/15\/ownership-and-borrowing-in-d\/ Accessed: 2021-01-05  Walter Bright. 2019. Ownership and Borrowing in D. https:\/\/web.archive.org\/web\/20210105083139\/https:\/\/dlang.org\/blog\/2019\/07\/15\/ownership-and-borrowing-in-d\/ Accessed: 2021-01-05"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/249069.231395"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645867.670924"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.5"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_2_2_23_1","volume-title":"Chez Scheme Version 9 User\u2019s Guide -","unstructured":"2017. Chez Scheme Version 9 User\u2019s Guide - Chapter 6. Control Structures . Available at https:\/\/cisco.github.io\/ChezScheme\/csug9.4\/control.html 2017. Chez Scheme Version 9 User\u2019s Guide - Chapter 6. Control Structures. Available at https:\/\/cisco.github.io\/ChezScheme\/csug9.4\/control.html"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2554511.2554516"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_11"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/583854.582447"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/646158.680008"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286947"},{"key":"e_1_2_2_29_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.  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_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341643"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1757028.1757039"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85373-2_12"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378811"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049709"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99608"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473576"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/277652.277748"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.10"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103796"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512563"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984042"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884002"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000040"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.18"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/118014.117975"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.375719"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.15"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428276"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500590"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/3271463"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.11.006"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_64_1","first-page":"73","article-title":"Separation logic for a higher-order typed language. In Workshop on Semantics, Program Analysis and Computing Environments for Memory Management","volume":"6","author":"Krishnaswami Neelakantan","year":"2006","unstructured":"Neelakantan Krishnaswami . 2006 . Separation logic for a higher-order typed language. In Workshop on Semantics, Program Analysis and Computing Environments for Memory Management , SPACE. 6 , 73 \u2013 82 . Neelakantan Krishnaswami. 2006. Separation logic for a higher-order typed language. In Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, SPACE. 6, 73\u201382.","journal-title":"SPACE."},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481874"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009872"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428243"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_21"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_71_1","volume-title":"ECOOP Workshop on Formal Techniques for Java Programs.","author":"M\u00fcller Peter","year":"2000","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. 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_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/646005.673740"},{"key":"e_1_2_2_74_1","unstructured":"James Noble. 2018. Two Decades of Ownership Types. In SPLASH-I. ACM.  James Noble. 2018. Two Decades of Ownership Types. In SPLASH-I. ACM."},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/646155.679699"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99590"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2591013"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004495"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00359-4"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984009"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987237.1987247"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.5555\/271338.271343"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.5555\/647323.721503"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.5555\/646243.681592"},{"key":"e_1_2_2_91_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984008"},{"key":"e_1_2_2_93_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.238"},{"key":"e_1_2_2_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/1631687.1596596"},{"key":"e_1_2_2_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/2184319.2184345"},{"key":"e_1_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429128"},{"key":"e_1_2_2_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-45221-5_47"},{"key":"e_1_2_2_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408975"},{"key":"e_1_2_2_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_2_2_100_1","doi-asserted-by":"publisher","DOI":"10.5555\/645394.651903"},{"key":"e_1_2_2_101_1","volume-title":"A principled design of capabilities in Pony. Master\u2019s thesis","author":"Steed George","unstructured":"George Steed and Sophia Drossopoulou . 2016. A principled design of capabilities in Pony. Master\u2019s thesis , Imperial College . George Steed and Sophia Drossopoulou. 2016. A principled design of capabilities in Pony. Master\u2019s thesis, Imperial College."},{"key":"e_1_2_2_102_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076021.2048142"},{"key":"e_1_2_2_103_1","unstructured":"The Swift Developer Community. 2019. Ownership Manifesto. https:\/\/github.com\/apple\/swift\/blob\/main\/docs\/OwnershipManifesto.md Accessed: 2021-04-09 (ae2a4cca14)  The Swift Developer Community. 2019. Ownership Manifesto. https:\/\/github.com\/apple\/swift\/blob\/main\/docs\/OwnershipManifesto.md Accessed: 2021-04-09 (ae2a4cca14)"},{"key":"e_1_2_2_104_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_2_105_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2018.01.001"},{"key":"e_1_2_2_106_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:3)2011"},{"key":"e_1_2_2_107_1","unstructured":"Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods. North-Holland 561.  Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods. North-Holland 561."},{"key":"e_1_2_2_108_1","doi-asserted-by":"publisher","DOI":"10.1145\/363911.363923"},{"key":"e_1_2_2_109_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408981"},{"key":"e_1_2_2_111_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_5"},{"key":"e_1_2_2_112_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"},{"key":"e_1_2_2_113_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2008.04.001"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485516","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485516","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485516","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485516"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":112,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485516"],"URL":"https:\/\/doi.org\/10.1145\/3485516","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}