Pith. sign in

REVIEW 4 major objections 5 minor 62 references

What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures (Extended Version)

T0 review · 4 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper introduces reach capabilities, a mechanism that names the capabilities hidden inside boxed generic data structures, and shows they make capture checking practical enough to compile Scala's standard collections library with minimal

desk verdict A serious, well-engineered paper that makes capture checking practical for generic data structures; the main open risk is that the surface calculus's soundness rests on an unmechanized translation and an intuitive deep-capture-set definition. read the letter →

arxiv 2509.07609 v1 pith:TXLDVK3R submitted 2025-09-09 cs.PL

Yichen Xu , Oliver Bračevac , Cao Nguyen Pham , Martin Odersky This is my paper
classification cs.PL
keywords capturecheckingreachcapabilitieseffectpolymorphismgenericdatastructurescapturingtypesScala3typesoundness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Capturing types track effects and resources by recording which capability variables a value captures. When such values sit inside generic data structures, their capabilities are hidden in boxes and lose their names, so functions over collections of effectful values (like a Set[Future[T]]) are either rejected or given imprecise types. This paper argues that reach capabilities fix that: when a variable is used, the type checker refines the universal capability inside its type to a new name x*, making 'what's in the box' addressable, while the @use annotation forces call sites to account for the argument's deep capture set. The paper grounds this design in System Capless, a calculus with explicit existential and universal capture-set quantification, and shows by a type-preserving translation that the lightweight surface syntax is exactly that calculus in disguise. The payoff is empirical: the full Scala collections library compiles under capture checking with under 5% of lines changed and almost 90% of function signatures unmodified, making effect tracking a realistic option for mainstream code.

What carries the argument

The central object is the reach capability x* — a name for what is inside the box. When x is used, reach refinement replaces covariant occurrences of the universal capability cap in x's type with x*, making a generic collection's hidden captures addressable. The deep capture set dcs(Γ,T) collects the capabilities occurring covariantly in T and is the concrete witness when a reach capability is instantiated at a call site; the @use annotation tells the checker to add the argument's deep capture set to the caller's capture set. System Capless grounds this by translating hidden caps into explicit existential or universal capture quantifiers, making the naming sound.

What would settle it

Give a @use parameter a boxed value whose type mentions a capability only contravariantly (e.g., a stored function File^ => Unit), then invoke that function with a file inside the body. If the resulting capture set omits the file effect, dcs is unsound; if the checker rejects the program, dcs over-approximates. Either outcome would settle whether dcs correctly characterizes what's in the box.

Watch

Extended reading notes

Core claim

Reach capabilities make effect polymorphism over generic data structures expressive yet lightweight. A reach capability x* names the existential capture set hidden in the boxes of x's type: reach refinement replaces covariant occurrences of cap in x's type with x*; the deep capture set dcs(Γ,T) collects the capabilities that can escape through a value of type T and instantiates x* at @use call sites; @use adds dcs to the caller's capture set. System Capless replaces cap with explicit universal/existential capture quantification; System Reacap translates to it type-preservingly. A Scala 3 reimplementation compiles the collections library with under 5% of lines changed.

Load-bearing premise

The whole mechanism rests on the assumption that the deep capture set — which collects only covariant capability occurrences in a type — captures every capability that can actually escape through a use of a value of that type, with no misses in contravariant or hidden positions and no harmful over-approximation.

Editorial extensions

If this is right

  • Functions such as mkIterator and collect get precise types like Iterator[T]^{ops*}; a pure input yields a pure result instead of an arbitrary top capture.
  • Scala's standard collections library compiles under capture checking with under 5% of lines changed and almost 90% of function signatures unmodified.
  • Explicit capture-set polymorphism becomes optional; the collections library required none, and recursive or mutable patterns can fall back to explicit capture parameters.
  • Capture checking can be adopted per module since checked and unchecked code can be mixed, and the mostly box-inferred syntax keeps most signatures untouched.
  • Lean-mechanized type soundness and scope safety provide a foundation for extending the system toward freshness, capability categories, and path-dependent capture tracking.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the deep-capture-set characterization is complete, the same recipe — removing the top capability, adding explicit capture quantifiers, and offering a surface-level reach name — should transplant to other box-based capability or effect systems.
  • Generalizing reach capabilities from whole variables to paths, as the paper's p._1* discussion suggests, would give element-level precision and directly address the coarse-grained fst/snd limitation the paper acknowledges.
  • A testable extension: applying the same migration recipe to other mainstream libraries (e.g., futures/IO ecosystems beyond the case study) would show whether the under-5%-changes figure is a property of the mechanism or of the collections library.
  • Because dcs is defined covariantly and no completeness theorem is given, the soundness boundary in contravariant or hidden positions remains the open question most likely to delimit the approach.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper develops System Capless, a capture calculus with explicit universal and existential capture-set quantification, and System Reacap, a surface calculus with reach capabilities (x*) and @use annotations. Reach capabilities are intended to name the contents of boxes in generic data structures without obliging users to write capture quantifiers. The authors report a Lean 4 mechanization of Capless type soundness and scope safety, a pen-and-paper type-preserving translation from Reacap to Capless, and a reimplementation of Scala 3's capture checker used to port the standard collections library with, they claim, minimal changes. The central claim is that reach capabilities make capture checking ergonomic and expressive enough for generic collections.

Significance. If the results hold, this is a substantial step toward practical effect/capture tracking in a mainstream language: it directly addresses a known limitation of prior capture-checking systems (CC<:□), provides a new foundational calculus with both existential and universal capture-set quantification, and validates the design on a large code base. The machine-checked metatheory for Capless and the artifact (Lean development, compiler, migrated collections) are genuine strengths. However, the surface language's soundness depends on a paper-and-pencil translation whose key cases are sketched, and on the deep-capture-set function dcs, which lacks a formal characterization tying it to the existential witnesses introduced by the translation. These gaps are load-bearing because the @use application rule and reach-capability semantics rely on dcs being exactly the set of escaping capabilities.

major comments (4)
  1. [Definition 4.1 / Figure 4 (app)] The soundness of reach capabilities rests on the claim that dcs(Γ,T) collects exactly the capabilities that can escape through a value of type T. Definition 4.1 is purely covariant: it discards z and z* from function results, ignores contravariant argument types, and for applied types sums only over covariant parameters. The paper provides examples but no theorem stating, for every type T and appropriate translation context, that dcs(Γ,T) matches the existential witness produced by the translation J T K. Without such a characterization, the (app) rule's use of dcs(Γ,S) both as a subcapturing obligation and as the substitution for z* is not justified. A reach capability hidden in a nested negative position (e.g., inside a box in a contravariant function argument of a result type) could be missed, reintroducing exactly the leaks that the earlier failures (#19571, #20503, #21442) exhibited.
  2. [Theorem 5.3 / Appendix D.3] Theorem 5.3 is the only bridge between Reacap's surface semantics and the mechanized Capless metatheory, yet its proof is not mechanized and several cases are only sketched. In the (app) case the proof constructs a term using D1 but does not show that D1 equals the translation of dcs(Γ,S_y); the closing note that 'the use set when typing t' will include D1' is not a derivation. In the (abs) case the two subcases (existential vs. non-existential result type) are handled differently, but the well-formedness of the extended contexts is not verified. Because subtyping in Reacap induces term transformations in Capless (Theorem D.10), these are not routine details. The central claim that Reacap is 'certified' by the translation is therefore not fully supported.
  3. [Theorem D.10 (Translation Preserves Subtyping)] This theorem is load-bearing because every use of (sub) in a Reacap derivation must be translated into a term transformation in Capless. The proof's (fun) case constructs a long eta-expansion with several let-bound intermediates but does not present the full typing derivation of that term. The (applied-p) and (applied-m) cases are dispatched with 'By induction ... we can construct a way adapt the term' and a note about decreasing the size of Θ. This is a proof sketch, not a proof. Since this theorem is outside the Lean development, the gap is not caught by the mechanization. Please provide complete proofs or extend the mechanization to cover the translation.
  4. [Table 2 / §7.2] The headline quantitative claims are difficult to verify from Table 2. The row 'Capture sets on definitions' reports 691 functions and 91 classes changed, while its two subcategories ('Only universal captures' = 351 and 'Only capture set on returns' = 379) sum to 730, exceeding 691. It is unclear whether the 691 counts only functions or also includes classes, and whether the subcategories are disjoint. The 25 'Unsafe capture set removal' and 5 'Unsafe casts' are escape hatches, but their locations and necessity are not discussed, which weakens the claim of a sound capture-checked library. Finally, the abstract's '<5% LoC changed' and 'almost 90% function signatures stay the same' are not reproduced by the table: 2825 changed lines / 52,160 total lines = 5.4%, and 691 changed functions / 6189 functions = 11.2% changed (88.8% unchanged). Please clarify the denominators and make the change
minor comments (5)
  1. [Section 5, first sentence] Typo: 'scope safey' should be 'scope safety'.
  2. [Section 7.1, Table 1] The text says capture checking takes 'approximately half the time compared to the previous typing phase'; Table 1 shows 3896 ms vs. 10436 ms, which is about 37%, not half. Please adjust the wording.
  3. [References [43, 44, 23]] The cited GitHub issues are labeled '2015' but issue numbers 19571, 20503, and 21442 correspond to a much later period. Please correct the years.
  4. [Data Availability] The artifact DOI is given, but the paper does not include a commit hash, Lean version, or verification instructions. Adding these would materially improve reproducibility.
  5. [Definition 4.1] In dcs(Γ,∀α(z:T)U) = dcs(Γ,U)\ {z,z*}, the removal of z from the capture set of U is intuitive but should be justified explicitly: a function result mentioning z refers to the parameter, not to an escaping capability. A short explanation would prevent confusion.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the rcaps mechanism is assigned meaning by a type-preserving translation into a separately mechanized calculus, and no fitted parameter is renamed as a prediction.

full rationale

The paper's central construction is System Reacap, whose reach capabilities are not assumed sound but are assigned meaning by the type-preserving translation (Theorem 5.3) into System Capless, whose type soundness and scope safety are independently mechanized in Lean 4. The deep capture set dcs (Definition 4.1) is a syntactic definition used in the @use application rule; the paper does not prove a completeness theorem connecting dcs to the exact escaping capabilities, but that is a soundness/expressiveness gap rather than a circular reduction: nothing in the paper defines dcs in terms of the typing conclusion it is used to derive. The motivating examples are counterexamples to an earlier design, not fitted inputs. Prior work on CC<:□ [5] and the earlier rcaps extended abstract [55] are cited as building blocks and as evidence of previous soundness bugs, but the present derivation does not reduce to those citations: System Capless is new and has mechanized metatheory, and the library migration is an empirical existence proof rather than a prediction forced by construction. The pen-and-paper status of the translation theorem and the absence of a dcs characterization theorem are correctness risks, not circularity.

Assumptions & free parameters 0 free parameters · 6 assumptions · 2 invented entities

No numerical constants are fitted to data. The type-level variables, reach capabilities, and capture-set quantifiers are syntax, not free parameters. The axioms listed are the substantive domain assumptions that the central claim depends on, plus the unmechanized translation proof that transfers soundness from Capless to Reacap.

assumptions (6)
  • domain assumption Capabilities are represented as ordinary program variables, and a capturing type over-approximates the variables a value may capture (object-capability model).
    This is the foundation inherited from CT and CC<:□ (Sections 2.1, refs [5,33]); the entire meaning of capture sets rests on it.
  • domain assumption Generic type arguments are boxed by default; box inference is complete and boxes have no runtime cost.
    Introduced in Section 2.1.3 and implemented by [56]; the practical scalability and 'signatures stay the same' claims depend on box inference being complete and transparent.
  • domain assumption Deep capture sets dcs(Γ,T), collecting only covariant capture occurrences, characterize exactly the capabilities accessible by unboxing or using a value of type T.
    Definition 4.1 and Section 2.2.2; the @use application rule and reach-capability instantiation depend on this equivalence. This is the weakest load-bearing premise.
  • domain assumption Reach refinement can safely replace covariant occurrences of cap by x*, excluding function domains and codomains, with type definitions recovering lost expressiveness.
    Section 4.2.3 and Appendix B.3; unless this restricted refinement covers the patterns of interest, rcaps would not support the claimed programming patterns.
  • ad hoc to paper The type-preserving translation from Reacap to Capless (Theorem 5.3) is correct as a paper-and-pencil proof.
    The surface calculus's soundness is inherited from the core via this translation; the proof is not mechanized and contains sketched cases in Appendix D.
  • standard math Standard syntactic type-soundness machinery (progress, preservation, store typing) applies.
    Used in Section 5; mechanized in Lean for System Capless and the scope-safety extension.
invented entities (2)
  • Reach capability x* independent evidence
    purpose: Names the existential capture set of capabilities inside boxes of a variable x, letting result types capture x* instead of {cap}.
    The compiler implementation and type-checking examples provide a falsifiable artifact; the semantics is given by translation to System Capless.
  • System Capless bounded capture quantification (universal and existential capture variables)
    purpose: Replaces the universal capability cap as an internal semantics, enabling precise capture polymorphism and the translation of rcaps.
    This is a mathematical entity inside the paper's own semantics; it has no observable handle separate from the calculus and its proofs.

how reviews work

0 comments
Cite this review

Pith. "Pith review of What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures (Extended Version)." pith.science (2026). https://pith.science/paper/TXLDVK3R

@misc{pith2026250907609,
  author       = {Pith},
  title        = {Pith review of: What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TXLDVK3R}},
  note         = {Machine review of arXiv:2509.07609}
}
read the original abstract

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 -- an essential prerequisite for broader adoption. This limitation stems from the inability to name capabilities within the system's notion of box types. 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 "what's in the box." 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. 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.

Figures

Figures reproduced from arXiv: 2509.07609 by the authors.

Figure 1
Figure 1. Abstract syntax of System Capless. Key differences from System CC [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Typing rules of System Capless. substitutions in dependent applications are always variable renamings and preserve the structure of types. The main difference stems from dropping the top capture set cap in favor of explicit bounded universal and existential capture quantification, which behave similarly to the respective quantifiers in System F≤ for types. Accordingly, capture sets 𝐶 can now also mention capture var… view at source ↗
Figure 3
Figure 3. Abstract syntax of System Reacap. {console, logger} though the latter did not use console. Besides, the premises and the conclusion share the same use set 𝐶, which is more uniform and streamlined. One can always find a use set that accounts for all the capabilities used by the premises and use (sub) to make this rule applicable. Beyond providing a theoretical basis for rcaps, System Capless itself is a more principl… view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: Static semantics of System Reacap. 4.2.3 Reach Refinement. Reach refinement 𝐶 ⊢ 𝑇 { 𝑈 replaces certain covariant occurrences of cap in type 𝑇 with the capture set 𝐶, where 𝐶 is often the reach capability of a variable (e.g., in the (var) rule). As shown in [PITH_FULL_…
Figure 5
Figure 5. Figure 5: Extensions to static rules of Capless. at the type level with no corresponding term representation that could be transformed during translation. For instance, consider a type function 𝑓 : ∀[𝑋 <: (IO ∧ {io} → Unit)] . . . and an application 𝑓 [IO∧ {cap} → Unit], where I…
Figure 6
Figure 6. Figure 6: Definition of well-formedness of System Capless. [PITH_FULL_IMAGE:figures/full_fig_p029_6.png]
Figure 7
Figure 7. Figure 7: Definition of well-formedness of System Reacap. [PITH_FULL_IMAGE:figures/full_fig_p029_7.png]
Figure 8
Figure 8. Figure 8: Well-formedness of type definitions. Syntax Σ B Store ∅ empty Σ, val 𝑥 ↦→ 𝑣 val binding Ψ B Evaluation Context [ ] hole let 𝑥 = Ψ in 𝑡 let let ⟨𝑐, 𝑥 ⟩ = Ψ in 𝑡 ex. let Reduction ⟨Σ | 𝑡⟩ −→ ⟨Σ ′ | 𝑡 ′ ⟩ Σ(𝑥 ) = 𝜆(𝑧 : 𝑇 )𝑡 ⟨Σ | Ψ[𝑥 𝑦] ⟩ −→ ⟨Σ | Ψ[ [𝑧 := 𝑦]𝑡] ⟩ (apply) Σ(…
Figure 9
Figure 9. Figure 9: Evaluation rules of System Capless. Changes from System CC [PITH_FULL_IMAGE:figures/full_fig_p030_9.png]
Figure 10
Figure 10. Figure 10: Extensions to dynamic rules of Capless. A.2 Reduction Rules of System Capless [PITH_FULL_IMAGE:figures/full_fig_p031_10.png]
Figure 11
Figure 11. Figure 11: Store Typing [PITH_FULL_IMAGE:figures/full_fig_p033_11.png]
Figure 12
Figure 12. Figure 12: Semantics of System Decap Definition D.1 (Translation Context). A translation context, denoted as ⟨𝐶, 𝜌, 𝜌∗ ⟩ and by the meta-variable 𝜏, consists of the following components: • a capture set 𝐷 in System Capless; • a function 𝜌 which maps term variable names to captur…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

62 extracted references · 56 canonical work pages

  1. [1]

    Parkinson, and Tobias Wrigstad

    Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson, and Tobias Wrigstad. 2023. Reference capabilities for flexible memory management. Proc. ACM Program. Lang. , 7, OOPSLA2, 1363–1393 (cit. on p. 25)

    work page 2023

  2. [2]

    Thibaut Balabonski, François Pottier, and Jonathan Protzenko. 2016. The design and formalization of Mezzo, a permission-based programming language. ACM Trans. Program. Lang. Syst. , 38, 4, 14:1–14:94 (cit. on p. 24)

    work page 2016

  3. [3]

    Yuyan Bao, Guannan Wei, Oliver Bračevac, 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 (cit. on p. 23)

    work page 2021

  4. [4]

    Erik Barendsen and Sjaak Smetsers. 1996. Uniqueness typing for functional languages with graph rewriting semantics. Math. Struct. Comput. Sci. , 6, 6, 579–612 (cit. on p. 24)

    work page 1996

  5. [5]

    Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondrej Lhoták, and Jonathan Immanuel Brachthäuser

  6. [6]

    Chandrasekhar Boyapati, Barbara Liskov, and Liuba Shrira. 2003. Ownership types for object encapsulation. In POPL. ACM, 213–223 (cit. on p. 24)

    work page 2003

  7. [7]

    Oliver Bračevac, 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 (cit. on p. 23)

    work page Pith review arXiv 2023

  8. [8]

    Oliver Bračevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao, and Tiark Rompf. 2023. Graph IRs for impure higher-order languages: Making aggressive optimizations affordable with precise effect dependencies. Proc. ACM Program. Lang., 7, OOPSLA2, 400–430 (cit. on p. 23)

    work page 2023

Show all 62 references
  1. [9]

    Jonathan Immanuel Brachthäuser, 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 (cit. on pp. 1, 2, 24)

    2022

  2. [10]

    Jonathan Immanuel Brachthäuser, 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 (cit. on pp. 1, 2)

    2020

  3. [11]

    Canthrow capabilities

    2021. Canthrow capabilities. Accessed: 2025-07-28. https://docs.scala-lang.org/scala3/reference/experimental/canthr ow.html (cit. on p. 24)

    2021

  4. [12]

    Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. 2013. Ownership types: A survey. In Aliasing in Object-Oriented Programming. Lecture Notes in Computer Science. Vol. 7850. Springer, 15–58 (cit. on p. 24)

    2013

  5. [13]

    Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015. Deny capabilities for safe, fast actors. In AGERE!@SPLASH. ACM, 1–12 (cit. on p. 24)

    2015

  6. [14]

    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 (cit. on p. 24)

    2017

  7. [15]

    Lukas Convent, Sam Lindley, Conor McBride, and Craig McLaughlin. 2020. Doo bee doo bee doo. J. Funct. Program., 30, e9 (cit. on pp. 1, 2, 25)

    2020

  8. [16]

    Werner Dietl, Sophia Drossopoulou, and Peter Müller. 2007. Generic universe types. In ECOOP (Lecture Notes in Computer Science). Vol. 4609. Springer, 28–53 (cit. on p. 24)

    2007

  9. [17]

    Fish, Darya Melicher, and Jonathan Aldrich

    Jennifer A. Fish, Darya Melicher, and Jonathan Aldrich. 2020. A case study in language-based security: Building an I/O library for Wyvern. In Onward! ACM, 34–47 (cit. on p. 25)

    2020

  10. [18]

    Foster, Manuel Fähndrich, and Alexander Aiken

    Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. 1999. A theory of type qualifiers. In PLDI. ACM, 192–203 (cit. on p. 25). What’s in the Box 334:27

    1999

  11. [19]

    Colin S. Gordon. 2020. Designing with Static Capabilities and Effects: Use, Mention, and Invariants. In 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs)). Robert Hirschfeld and Tobias Pape, (Eds.) V...

    2020 doi

  12. [20]

    Gregory Morrisett, Trevor Jim, Michael W

    Dan Grossman, J. Gregory Morrisett, Trevor Jim, Michael W. Hicks, Yanling Wang, and James Cheney. 2002. Region- based memory management in Cyclone. In PLDI. ACM, 282–293 (cit. on p. 24)

    2002

  13. [21]

    John Hatcliff and Olivier Danvy. 1994. A generic account of continuation-passing styles. InPOPL. ACM Press, 458–471 (cit. on pp. 10, 13)

    1994

  14. [22]

    Mark P. Jones. 1994. A theory of qualified types. Sci. Comput. Program., 22, 3, 231–256 (cit. on p. 25)

    1994

  15. [23]

    Leaking local reach capability

    2015. Leaking local reach capability. Accessed: 2025-03-23. https://github.com/scala/scala3/issues/21442 (cit. on pp. 3, 8)

    2015

  16. [24]

    Edward Lee, Yaoyu Zhao, Ondrej Lhoták, James You, Kavin Satheeskumar, and Jonathan Immanuel Brachthäuser

  17. [25]

    Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. In POPL. ACM, 500–514 (cit. on pp. 1, 2, 25)

    2017

  18. [26]

    Eisenberg, and Sam Lindley

    Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, and Sam Lindley. 2024. Oxidizing OCaml with modal memory management. Proc. ACM Program. Lang., 8, ICFP, Article 253, (Aug. 2024), 30 pages (cit. on p. 25)

    2024

  19. [27]

    Lucassen and David K

    John M. Lucassen and David K. Gifford. 1988. Polymorphic effect systems. In POPL. ACM Press, 47–57 (cit. on p. 24)

    1988

  20. [28]

    Matthew Lutze and Magnus Madsen. 2024. Associated effects: Flexible abstractions for effectful programming. Proc. ACM Program. Lang., 8, PLDI, 394–416 (cit. on p. 25)

    2024

  21. [29]

    Danielle Marshall, Michael Vollmer, and Dominic Orchard. 2022. Linearity and uniqueness: An entente cordiale. In ESOP (Lecture Notes in Computer Science). Vol. 13240. Springer, 346–375 (cit. on p. 24)

    2022

  22. [30]

    Matsakis and Felix S

    Nicholas D. Matsakis and Felix S. Klock II. 2014. The Rust language. In HILT. ACM, 103–104 (cit. on p. 24)

    2014

  23. [31]

    Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. 2017. A capability-based module system for authority control. In ECOOP (LIPIcs). Vol. 74. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 20:1–20:27 (cit. on p. 25)

    2017

  24. [32]

    Darya Melicher, Anlun Xu, Valerie Zhao, Alex Potanin, and Jonathan Aldrich. 2022. Bounded abstract effects. ACM Trans. Program. Lang. Syst., 44, 1, 5:1–5:48 (cit. on p. 25)

    2022

  25. [33]

    Mark S. Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control . Ph.D. Dissertation. John Hopkins University (cit. on pp. 1, 25)

    2006

  26. [34]

    Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory.ACM Trans. Comput. Log., 9, 3, 23:1–23:49 (cit. on p. 24)

    2008

  27. [35]

    James Noble, Jan Vitek, and John Potter. 1998. Flexible alias protection. In ECOOP (Lecture Notes in Computer Science). Vol. 1445. Springer, 158–185 (cit. on p. 24)

    1998

  28. [36]

    Robert Nystrom. 2015. What colour is your function? Accessed: 2024-09-09. https://web.archive.org/web/2024100915 2925/https://journal.stuffwithstuff.com/2015/02/01/what-color-is-your-function/ (cit. on p. 23)

    2015

  29. [37]

    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 (cit. on p. 18)

    2018

  30. [38]

    Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondrej Lhoták

  31. [39]

    Essertel, Xilun Wu, Lilliam I

    Leo Osvald, Grégory M. Essertel, Xilun Wu, Lilliam I. González Alayón, and Tiark Rompf. 2016. Gentrification gone too far? Affordable 2nd-class values for fun and (co-)effect. In OOPSLA. ACM, 234–251 (cit. on p. 25)

    2016

  32. [40]

    Cao Nguyen Pham and Martin Odersky. 2024. Stack-copying delimited continuations for Scala Native. In ICOOOLPS @ ECOOP. ACM, 2–13. doi: 10.1145/3679005.3685979 (cit. on p. 24)

    2024

  33. [41]

    url: https://web.archive.org/web/20 241007175842/https://www.ponylang.io/, vcs: https://github.com/ponylang/ponyc (cit

    [SW Mod.] Pony, Pony Programming Language 2024 Pony Development Team. url: https://web.archive.org/web/20 241007175842/https://www.ponylang.io/, vcs: https://github.com/ponylang/ponyc (cit. on p. 24)

    2024

  34. [42]

    Alex Potanin, James Noble, Dave Clarke, and Robert Biddle. 2006. Generic ownership for generic Java. In OOPSLA. ACM, 311–324 (cit. on p. 24)

    2006

  35. [43]

    Reach capabilities get dropped in cv

    2015. Reach capabilities get dropped in cv. Accessed: 2025-03-23. https://github.com/scala/scala3/issues/19571 (cit. on pp. 3, 8)

    2015

  36. [44]

    Reach capabilities of function arguments get ignored

    2015. Reach capabilities of function arguments get ignored. Accessed: 2025-03-23. https://github.com/scala/scala3/iss ues/20503 (cit. on pp. 3, 8)

    2015

  37. [45]

    Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In OOPSLA. ACM, 624–641 (cit. on pp. 22, 25). 334:28 Yichen Xu, Oliver Bračevac, Cao Nguyen Pham, and Martin Odersky

    2016

  38. [46]

    Jean-Pierre Talpin and Pierre Jouvelot. 1994. The type and effect discipline. Inf. Comput., 111, 2, 245–296 (cit. on p. 24)

    1994

  39. [47]

    Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, and Anton Lorenzen. 2025. Modal effect types. Proc. ACM Program. Lang., 9, OOPSLA1, Article 120, (Apr. 2025), 28 pages. doi: 10.1145/3720476 (cit. on pp. 1, 2, 25)

    2025 doi

  40. [48]

    Mads Tofte and Jean-Pierre Talpin. 1997. Region-based memory management. Inf. Comput., 132, 2, 109–176 (cit. on p. 24)

    1997

  41. [49]

    Philip Wadler. 1990. Linear types can change the world! In Programming Concepts and Methods . North-Holland, 561 (cit. on p. 24)

    1990

  42. [50]

    Philip Wadler. 1989. Theorems for free! InProceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA ’89). Association for Computing Machinery, Imperial College, London, United Kingdom, 347–359. isbn: 0897913280. doi:...

    1989

  43. [51]

    Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, and Tiark Rompf. 2024. Polymorphic reachability types: Tracking freshness, aliasing, and separation in higher-order generic programs. Proc. ACM Program. Lang., 8, POPL, 393–424 (cit. on p. 23)

    2024

  44. [52]

    Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, and Tiark Rompf. 2022. What if we don’t pop the stack? The return of 2nd-class values. In ECOOP (LIPIcs). Vol. 222. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 15:1–15:29 (cit. on p. 25)

    2022

  45. [53]

    Yichen Xu, Aleksander Boruch-Gruszecki, and Martin Odersky. 2024. Degrees of separation: A flexible type system for safe concurrency. Proc. ACM Program. Lang., 8, OOPSLA1, 1181–1207. doi: 10.1145/3649853 (cit. on p. 23)

    2024 doi

  46. [54]

    What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures

    [SW] Yichen Xu, Oliver Bračevac, Cao Nguyen Pham, and Martin Odersky, Artifact for "What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures" Aug. 2025. doi: 10.5281/zenodo.16922930 (cit. on pp. 4, 26)

    2025 doi

  47. [55]

    Yichen Xu and Martin Odersky. 2024. A formal foundation of reach capabilities (extended abstract). In Companion Proceedings of the International Conference on the Art, Science, and Engineering of Programming (VIMPL’24) . ACM. doi: 10.1145/3660829.3660851 (cit. on p. 3)

    2024

  48. [56]

    test.txt

    Yichen Xu and Martin Odersky. 2023. Formalizing box inference for capture calculus. ArXiv, abs/2306.06496 (cit. on p. 6). What’s in the Box 334:29 A Additional Definitions A.1 Well-formedness Γ⊢⊤ wf (wf-top) 𝑋 <:𝑆∈ Γ Γ⊢𝑋 wf (wf-tvar) Γ⊢𝑇 wf (Γ,𝑥 :𝑇)⊢ 𝐸 wf Γ⊢∀( 𝑥 :𝑇)𝐸 wf (wf-fu...

    2023 arXiv

  49. [60]

    Case (box)

    We then conclude this case by Theorem D.10 and Theorem D.2. Case (box). Then the typing derivation is of the form{}; Γ⊢ □𝑥0 : □(𝑆0∧𝐶0) where we have 𝐶0; Γ⊢𝑥0 :𝑆0∧𝐶0. By the IH, we can show that J𝐶0K𝐷0; Δ⊢𝑎′ 0 : J𝑆0∧𝐶0K𝐷0 for some𝐷0 and𝑎′

  50. [61]

    We conclude this case by repeated application of the (tabs) rule

    We let𝐷′ =𝐷0 and construct the following𝑡′: 𝜆[𝑋 <:⊤]𝜆[𝑋 <:⊤]𝑎′ 0, which is also an answer. We conclude this case by repeated application of the (tabs) rule. Case (unbox). Then the typing derivation is of the form 𝐶0; Γ⊢𝐶 𝑥0 :𝑆0∧𝐶0 and we have 𝐶0; Γ⊢𝑥0 : □𝑆0∧𝐶0. By analyzing th...

  51. [62]

    We construct the following𝑡′: let𝑧1 =𝑡′ 1 in 𝑡′ 2 and conclude this case by the (let) rule. If the second case holds, we invoke the IH on the second typing derivation to show that J𝐶K𝐷2; Δ,𝑐𝑧 : CapSet,𝑧 : J𝑇1K𝑐𝑧⊢𝑡′ 2 : J𝑇2K𝐷2 for some𝐷2 and𝑡′ 2, and construct the following𝑡′: ...

    2025

  52. [2021]

    In SCALA/SPLASH

    Safer exceptions for Scala. In SCALA/SPLASH. ACM, 1–11 (cit. on pp. 4, 24)

  53. [2023]

    ACM Trans

    Capturing types. ACM Trans. Program. Lang. Syst. , 45, 4, 21:1–21:52 (cit. on pp. 1, 2, 4, 6, 7, 10, 12–14, 17, 25, 30, 32)

  54. [2024]

    Qualifying system F<: Some terms and conditions may apply. Proc. ACM Program. Lang., 8, OOPSLA1, 583–612 (cit. on p. 25)

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.