{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:51Z","timestamp":1780994751127,"version":"3.54.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"FNSNF","award":["TMAG-2_209506\/1"],"award-info":[{"award-number":["TMAG-2_209506\/1"]}]}],"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>Capturing types in Scala unify static effect and resource tracking with object capabilities, enabling lightweight effect polymorphism with minimal notational overhead. However, their expressiveness has been insufficient for tracking capabilities embedded in generic data structures, preventing them from scaling to the standard collections library \u2013 an essential prerequisite for broader adoption. This limitation stems from the inability to name capabilities within the system\u2019s notion of box types.<\/jats:p>\n          <jats:p>This paper develops System Capless, a new foundation for capturing types that provides the theoretical basis for reach capabilities (rcaps), a novel mechanism for naming \u201cwhat\u2019s in the box\u201d. The calculus refines the universal capability notion into a new scheme with existential and universal capture set quantification. Intuitively, rcaps witness existentially quantified capture sets inside the boxes of generic types in a way that does not require exposing existential capture types in the surface language. We have fully mechanized the formal metatheory of System Capless in Lean, including proofs of type soundness and scope safety. System Capless supports the same lightweight notation of capturing types plus rcaps, as certified by a type-preserving translation, and also enables fully optional explicit capture-set quantification to increase expressiveness.<\/jats:p>\n          <jats:p>Finally, we present a full reimplementation of capture checking in Scala 3 based on System Capless and migrate the entire Scala collections library and an asynchronous programming library to evaluate its practicality and ergonomics. Our results demonstrate that reach capabilities enable the adoption of capture checking in production code with minimal changes and minimal-to-zero notational overhead in a vast majority of cases.<\/jats:p>","DOI":"10.1145\/3763112","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"1726-1753","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["What\u2019s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2089-6767","authenticated-orcid":false,"given":"Yichen","family":"Xu","sequence":"first","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"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\/0009-0005-2543-3309","authenticated-orcid":false,"given":"Cao Nguyen","family":"Pham","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3923-8993","authenticated-orcid":false,"given":"Martin","family":"Odersky","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"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","DOI":"10.1145\/3622846"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_2_1_3_1","first-page":"1","article-title":"Reachability types: Tracking aliasing and separation in higher-order functional programs","author":"Bao Yuyan","year":"2021","unstructured":"Yuyan Bao, Guannan Wei, Oliver Bra\u010devac, Yuxuan Jiang, Qiyang He, and Tiark Rompf. 2021. Reachability types: Tracking aliasing and separation in higher-order functional programs. Proc. ACM Program. Lang., 5, OOPSLA, 1-32.","journal-title":"Proc. ACM Program. Lang., 5, OOPSLA"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_1_6_1","first-page":"213","article-title":"Ownership types for object encapsulation. ACM","author":"Boyapati Chandrasekhar","year":"2003","unstructured":"Chandrasekhar Boyapati, Barbara Liskov, and Liuba Shrira. 2003. Ownership types for object encapsulation. ACM, In POPL. 213-223.","journal-title":"POPL."},{"key":"e_1_2_1_7_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 (Technical Report). CoRR abs\/2309.08118."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622813"},{"key":"e_1_2_1_9_1","first-page":"1","article-title":"Effects, capabilities, and boxes: From scope-based reasoning to type-based reasoning and back","author":"Brachth\u00e4user Jonathan Immanuel","year":"2022","unstructured":"Jonathan Immanuel Brachth\u00e4user, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki. 2022. Effects, capabilities, and boxes: From scope-based reasoning to type-based reasoning and back. Proc. ACM Program. Lang., 6, OOPSLA, 1-30.","journal-title":"Proc. ACM Program. Lang., 6, OOPSLA"},{"key":"e_1_2_1_10_1","first-page":"1","article-title":"Effects as capabilities: Effect handlers and lightweight effect polymorphism","volume":"126","author":"Brachth\u00e4user Jonathan Immanuel","year":"2020","unstructured":"Jonathan Immanuel Brachth\u00e4user, Philipp Schuster, and Klaus Ostermann. 2020. Effects as capabilities: Effect handlers and lightweight effect polymorphism. Proc. ACM Program. Lang., 4, OOPSLA, 126:1-126:30.","journal-title":"Proc. ACM Program. Lang., 4, OOPSLA"},{"key":"e_1_2_1_11_1","unstructured":"2021. CanThrow Capabilities. Accessed: 2025-07-28 https:\/\/docs.scala-lang.org\/scala3\/reference\/experimental\/canthrow.html"},{"key":"e_1_2_1_12_1","volume-title":"Ownership Types: A Survey","author":"Clarke Dave","year":"2013","unstructured":"Dave Clarke, Johan \u00d6stlund, Ilya Sergey, and Tobias Wrigstad. 2013. Ownership Types: A Survey. Springer, In Aliasing in Object-Oriented Programming (Lecture Notes in Computer Science, Vol. 7850). 15-58."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Sylvan Clebsch Sophia Drossopoulou Sebastian Blessing and Andy McNeil. 2015. Deny capabilities for safe fast actors. ACM In AGERE!@SPLASH. 1-12.","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_2_1_14_1","first-page":"1","article-title":"Orca: GC and type system co-design for actor languages","volume":"72","author":"Clebsch Sylvan","year":"2017","unstructured":"Sylvan Clebsch, Juliana Franco, Sophia Drossopoulou, Albert Mingkun Yang, Tobias Wrigstad, and Jan Vitek. 2017. Orca: GC and type system co-design for actor languages. Proc. ACM Program. Lang., 1, OOPSLA, 72:1-72:28.","journal-title":"Proc. ACM Program. Lang., 1, OOPSLA"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000039"},{"key":"e_1_2_1_16_1","volume-title":"Generic Universe Types","author":"Dietl Werner","unstructured":"Werner Dietl, Sophia Drossopoulou, and Peter M\u00fcller. 2007. Generic Universe Types. Springer, In ECOOP (Lecture Notes in Computer Science, Vol. 4609). 28-53."},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Jennifer A. Fish Darya Melicher and Jonathan Aldrich. 2020. A case study in language-based security: Building an I\/O library for Wyvern. ACM In Onward!. 34-47.","DOI":"10.1145\/3426428.3426913"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301665"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.10"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_1_21_1","volume-title":"A Generic Account of Continuation-Passing Styles","author":"Hatcliff John","unstructured":"John Hatcliff and Olivier Danvy. 1994. A Generic Account of Continuation-Passing Styles. ACM Press, In POPL. 458-471."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00005-0"},{"key":"e_1_2_1_23_1","unstructured":"2015. Leaking local reach capability. Accessed: 2025-03-23 https:\/\/github.com\/scala\/scala3\/issues\/21442"},{"key":"e_1_2_1_24_1","volume-title":"Proc. ACM Program. Lang., 8, OOPSLA1, 583-612","author":"Lee Edward","year":"2024","unstructured":"Edward Lee, Yaoyu Zhao, Ondrej Lhot\u00e1k, James You, Kavin Satheeskumar, and Jonathan Immanuel Brachth\u00e4user. 2024. Qualifying System F_ <: Some Terms and Conditions May Apply. Proc. ACM Program. Lang., 8, OOPSLA1, 583-612."},{"key":"e_1_2_1_25_1","first-page":"500","article-title":"Do be do be do. ACM","author":"Lindley Sam","year":"2017","unstructured":"Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. ACM, In POPL. 500-514.","journal-title":"POPL."},{"key":"e_1_2_1_26_1","volume-title":"Oxidizing OCaml with Modal Memory Management","author":"Lorenzen Anton","unstructured":"Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, and Sam Lindley. 2024. Oxidizing OCaml with Modal Memory Management. Association for Computing Machinery, Article 253, 30 pages. Proc. ACM Program. Lang., 8, ICFP."},{"key":"e_1_2_1_27_1","volume-title":"Gifford","author":"Lucassen John M.","year":"1988","unstructured":"John M. Lucassen and David K. Gifford. 1988. Polymorphic Effect Systems. ACM Press, In POPL. 47-57."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656393"},{"key":"e_1_2_1_29_1","volume-title":"Linearity and Uniqueness: An Entente Cordiale","author":"Marshall Danielle","unstructured":"Danielle Marshall, Michael Vollmer, and Dominic Orchard. 2022. Linearity and Uniqueness: An Entente Cordiale. Springer, In ESOP (Lecture Notes in Computer Science, Vol. 13240). 346-375."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_31_1","volume-title":"ECOOP (LIPIcs","volume":"27","author":"Melicher Darya","year":"2017","unstructured":"Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. 2017. A Capability-Based Module System for Authority Control. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, In ECOOP (LIPIcs, Vol. 74). 20:1-20:27."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3492427"},{"key":"e_1_2_1_33_1","volume-title":"Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control","author":"Miller Mark S.","year":"2006","unstructured":"Mark S. Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. John Hopkins University."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_35_1","volume-title":"Flexible Alias Protection","author":"Noble James","unstructured":"James Noble, Jan Vitek, and John Potter. 1998. Flexible Alias Protection. Springer, In ECOOP (Lecture Notes in Computer Science, Vol. 1445). 158-185."},{"key":"e_1_2_1_36_1","unstructured":"Robert Nystrom. 2015. What Colour is Your Function? Accessed: 2024-09-09 https:\/\/web.archive.org\/web\/20241009152925\/https:\/\/journal.stuffwithstuff.com\/2015\/02\/01\/what-color-is-your-function\/"},{"key":"e_1_2_1_37_1","first-page":"1","article-title":"Simplicitly: Foundations and applications of implicit function types","volume":"42","author":"Odersky Martin","year":"2018","unstructured":"Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. 2018. Simplicitly: Foundations and applications of implicit function types. Proc. ACM Program. Lang., 2, POPL, 42:1-42:29.","journal-title":"Proc. ACM Program. Lang., 2, POPL"},{"key":"e_1_2_1_38_1","first-page":"1","article-title":"Safer exceptions for Scala. ACM","author":"Odersky Martin","year":"2021","unstructured":"Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachth\u00e4user, Edward Lee, and Ondrej Lhot\u00e1k. 2021. Safer exceptions for Scala. ACM, In SCALA\/SPLASH. 1-11.","journal-title":"SCALA\/SPLASH."},{"key":"e_1_2_1_39_1","first-page":"234","article-title":"Gentrification gone too far? Affordable 2nd-class values for fun and (co-)effect. ACM","author":"Osvald Leo","year":"2016","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. ACM, In OOPSLA. 234-251.","journal-title":"OOPSLA."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Cao Nguyen Pham and Martin Odersky. 2024. Stack-Copying Delimited Continuations for Scala Native. ACM In ICOOOLPS @ ECOOP. 12 pages. 2-13. doi:10.1145\/3679005.3685979 https:\/\/doi.org\/10.1145\/3679005.3685979 10.1145\/3679005.3685979","DOI":"10.1145\/3679005.3685979"},{"key":"e_1_2_1_41_1","unstructured":"Pony. 2024. Pony Programming Language. Pony Development Team. Accessed: 2024-10-07 https:\/\/web.archive.org\/web\/20241007175842\/https:\/\/www.ponylang.io\/"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167500"},{"key":"e_1_2_1_43_1","unstructured":"2015. Reach capabilities get dropped in cv. Accessed: 2025-03-23 https:\/\/github.com\/scala\/scala3\/issues\/19571"},{"key":"e_1_2_1_44_1","unstructured":"2015. Reach capabilities of function arguments get ignored. Accessed: 2025-03-23 https:\/\/github.com\/scala\/scala3\/issues\/20503"},{"key":"e_1_2_1_45_1","first-page":"624","article-title":"Type soundness for dependent object types (DOT). ACM","author":"Rompf Tiark","year":"2016","unstructured":"Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). ACM, In OOPSLA. 624-641.","journal-title":"OOPSLA."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720476"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_1_49_1","unstructured":"Philip Wadler. 1990. Linear Types can Change the World!. North-Holland In Programming Concepts and Methods. 561."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_1_52_1","volume-title":"ECOOP (LIPIcs","volume":"29","author":"Xhebraj Anxhelo","year":"2022","unstructured":"Anxhelo Xhebraj, Oliver Bra\u010devac, Guannan Wei, and Tiark Rompf. 2022. What If We Don\u2019t Pop the Stack? The Return of 2nd-Class Values. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, In ECOOP (LIPIcs, Vol. 222). 15:1-15:29."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649853"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16922930"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2509.07609"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3660829.3660851"},{"key":"e_1_2_1_57_1","unstructured":"Yichen Xu and Martin Odersky. 2023. Formalizing Box Inference for Capture Calculus. ArXiv abs\/2306.06496."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763112","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:48:00Z","timestamp":1760032080000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763112"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":57,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763112"],"URL":"https:\/\/doi.org\/10.1145\/3763112","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"}}]}}