Pith. sign in

REVIEW 3 major objections 5 minor 92 references

System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)

T0 review · 3 major / 5 minor · reviewed 2026-07-13 · grok-4.5

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

Pith's one-line read Selective substructural alias control can be retrofitted onto Scala capture checking without making exclusivity the default.

desk verdict Solid selective alias-control retrofit for Scala, with Lean-checked core soundness; end-to-end Scala/spawn packaging rests on unmechanized translation and informal checker correspondence. read the letter →

arxiv 2607.09383 v1 pith:76Z5AOBP submitted 2026-07-10 cs.PL

Yichen Xu , Oliver Bračevac , Cao Nguyen Pham , Yaoyu Zhao , Martin Odersky This is my paper · ORCID
classification cs.PL
keywords capturecheckingseparationfreshnesscapabilitiessubstructuraltypesScaladata-racefreedomsemanticsoundness
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

Languages like Scala already allow unrestricted aliasing and higher-order sharing. Substructural disciplines (uniqueness, separation, borrowing) usually demand global ownership rules that are hard to retrofit. This paper claims you can keep ordinary sharing as the default and still recover the key safety guarantees where they matter, by extending capture checking with tracked separation, consumption, freshness, and read-only access for capabilities. The surface language Capybara is translated into a smaller core calculus whose semantic model (mechanized in Lean 4) yields type safety, no use-after-free or double-free, immutability for read-only runs, and data-race freedom for well-typed concurrent programs. The same ideas ship as Scala 3's separation checker, so ordinary Scala can enforce resource and concurrency contracts at APIs without rewriting the language's programming model.

What carries the argument

The type-preserving translation from Capybara to CoreCapybara: any becomes universal capture quantification, fresh becomes existential packing/unpacking, and separation obligations become constraint-indexed modal types [Ψ, Φ]E whose locks are discharged at call sites. Semantic typing of the core, plus confluence of reduction, carries the safety theorems.

What would settle it

A well-typed Capybara or Scala-3-checked program whose translated CoreCapybara run still exhibits a data race, use-after-free, double-free, or mutation through a read-only footprint would falsify the claimed transfer of guarantees.

Watch

Extended reading notes

Core claim

System Capybara shows that capture-checked capabilities, once extended with selective separation, consume/freshness, and read-only modes, recover the main reasoning principles of ownership and substructural type systems without imposing global exclusivity. A type-preserving translation into CoreCapybara, whose semantic soundness is proved in Lean 4, transfers type safety, memory safety, immutability of read-only computations, and data-race freedom to well-typed programs; the design is realized as Scala 3's separation checker.

Load-bearing premise

Surface and Scala-level safety is taken to follow from typing into the core alone; the paper does not define a surface operational semantics, prove semantic preservation, or formally relate the compiler checker to the calculi.

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

3 major / 5 minor

Summary. The paper presents System Capybara, a selective substructural layer on Scala-style capturing types that tracks separation, consumption, freshness, and read-only access for capabilities without imposing global ownership. It formalizes a surface calculus, a type-preserving translation into CoreCapybara (existentials, consumer lambdas, constraint-indexed modal locks, readers), and a step-indexed Kripke logical relation for the core, with Lean 4 mechanization of the fundamental theorem, adequacy, immutability, separation, standardization, and confluence. From these it derives type safety, memory safety (no use-after-free/double-free), read-only immutability, and data-race freedom for well-typed core programs, transferred to the surface via typability preservation (Thm 5.8 / C.4, Cor. C.5). A Scala 3 separation checker and case studies (builders, freeze, structured and spawn-style concurrency) illustrate the design.

Significance. If the core results and translation hold, this is a substantial contribution to retrofitting substructural reasoning into a mainstream higher-order language with pervasive sharing. The selective (API-local) discipline, root-based separation, and constraint-indexed modalities are a coherent alternative to global ownership or linear arrows, and the Lean mechanization of a higher-order-store model with footprints, killing, and concurrency is a real strength. The work also advances capture checking toward practical resource and concurrency safety. The main caveats are that end-to-end claims for ordinary Scala and outliving threads rest on an unmechanized paper translation and an informal checker correspondence, which the discussion acknowledges but the abstract packages more strongly.

major comments (3)
  1. §5.4, Thm 5.8 / Appendix C (esp. Lem C.21 ambient invariant, Rem C.2 ownership lock, Cor C.5): surface safety is transferred by type-preserving translation alone, with surface operational meaning defined as Core reduction of the translation and administrative forms argued to emit no heap events. There is no independent surface dynamics or semantic-preservation proof. The bridge is large, paper-only, and load-bearing for the abstract’s claim that well-typed Capybara programs enjoy the core guarantees; at least a clearer statement of what is and is not theorem-backed, or a mechanized fragment of the critical cases, is needed.
  2. §6.3.2 and §7: spawn consumes a closure whose thread may outlive the call, and the checker enforces consumption, but the formal model only covers structured par that joins before continuing. The abstract and intro package “fearless concurrency” and “ordinary Scala” more broadly than the theorems support. The manuscript should either restrict those claims to structured parallelism or make the gap between model and spawn-style APIs explicit in the contributions and abstract.
  3. §7 and §6.1: the Scala 3 separation checker (mode inference, peaks, killed peaks, Mutable/update/consume) is not formally related to the declarative calculi, and completeness/decidability are not proved. Case studies are useful but do not substitute for a correspondence argument if the paper’s selling point is bringing the formal guarantees to ordinary Scala. A short, precise statement of what is checked vs. what is proved would strengthen the contribution without overclaiming.
minor comments (5)
  1. Abstract and §1: “fearless concurrency” and “ordinary Scala” should be qualified to match §7’s scope (structured par; checker not formally related).
  2. Fig. 4 / running example: the surface–core alignment is helpful; a one-line pointer from §3.3 to the full translation trace in C.9 would help readers.
  3. Notation density in §3–4 (any/fresh instantiation, spine |T|, roots, ⊖, Ψ/Φ locks) is high; a short notation table early in §3 would improve accessibility.
  4. Related work §8: the contrast with OxCaml modes and Degrees of Separation is clear; a sentence on how constraint-indexed modalities relate to multimodal type theory would help specialists.
  5. Lean development is credited as AI-assisted for proof engineering; a brief note on what was human-checked vs. assisted would aid reproducibility expectations.

Circularity Check

1 steps flagged · score 1.0 of 10

No load-bearing circularity: Core soundness is a new Lean-checked model; surface transfer is standard elaboration, not a fit-or-definition loop.

  1. self citation load bearing [§1 contributions; §4 opening; Related Work §8 (Capless / capture checking)]
    "We define CoreCapybara, a compact core extending System Capless [89], and a type-preserving translation from Capybara to the core... Previous work on capture checking relied on syntactic type soundness [11, 89]. For Capybara, we instead give a semantic model of CoreCapybara..."

    CoreCapybara is presented as extending Capless [89] (overlapping authors). This is foundation reuse, not a circular step: the load-bearing soundness, separation, immutability, and confluence results are new semantic theorems about the extended core, not restatements forced by Capless’s prior definitions. Flagged only as minor same-group citation density; it does not collapse the claimed derivation.

full rationale

This is a type-system design paper whose central chain is (i) a new semantic model of CoreCapybara (footprints, kill, modal separation, sequential big-step + confluence), mechanized in Lean 4 (Thm 5.1–5.7 / App. B), and (ii) a type-preserving translation from surface Capybara that transfers those theorems (Thm 5.8 / C.4, Cor. C.5). Prior capture-checking / Capless results [11, 89] and degrees of separation [88] are cited as foundation; that is normal cumulative work, not a uniqueness theorem that forces the new concurrency/memory claims. The paper does not fit parameters to data or rename an empirical pattern as a prediction. Defining surface operational meaning via the translation (Cor. C.5; §7 admits no separate surface opsem or semantic preservation) is standard elaboration, not self-definitional circularity of the form “X predicts Y where Y is the fit of X.” Implementation correspondence to Scala 3 and spawn-style concurrency are explicitly out of the formal model (§7)—a scope gap, not a circular derivation. Score 1 only for heavy same-group foundation citations that are not load-bearing for the new theorems.

Assumptions & free parameters 0 free parameters · 5 assumptions · 3 invented entities

No empirical free parameters. The central claims rest on standard PL metatheory machinery plus design conventions of the surface language and the transfer principle that type-preserving translation plus core soundness yields surface guarantees. Invented entities are the calculi and checker themselves—standard for a language-design paper, with independent evidence only insofar as the Lean development and compiler implementation exist outside the prose.

assumptions (5)
  • standard math Step-indexed Kripke logical relations over higher-order store adequately capture safety of CoreCapybara (model of §5 / App. B).
    Standard technique (Ahmed, Appel–McAllester, Timany et al.); used as the soundness method rather than an ad-hoc postulate.
  • domain assumption Root-directedness, domain honesty, ambient-context, and canonical-derivation conventions for the surface calculus (App. C.1).
    Restrict which surface types/derivations are considered so any/fresh map cleanly to quantifiers and locks; load-bearing for the translation theorem.
  • ad hoc to paper Type-preserving translation transfers operational safety properties to surface programs without a surface semantics or semantic-preservation proof (§7, Cor. C.5).
    Explicit methodological choice; administrative reductions are argued not to emit heap events, but this is not a full semantic correspondence.
  • domain assumption Well-formed concurrent runs never block on authorization/non-interference guards when well-typed; confluence implies data-race freedom (Thm 5.5–5.7).
    Standard operational reading of race freedom as schedule-unobservability; depends on the footprint interpretation of separation.
  • ad hoc to paper Scala 3 checker behavior (mode inference, peaks, killed peaks) matches the declarative rules closely enough for the case studies (§6–7).
    No formal checker soundness/completeness proof; implementation is presented as guided by the core.
invented entities (3)
  • System Capybara surface calculus (separation, consume, fresh, ro on capturing types)
    purpose: Selective substructural API contracts on top of capture checking
    Primary design object of the paper; evidence is formal rules plus examples, not external measurement.
  • CoreCapybara (existentials, consumer lambdas, constraint-indexed modal locks, readers)
    purpose: Compact target for translation and semantic soundness
    Extends Capless; independent handle would be a public Lean module others can compile.
  • Scala 3 separation checker (Mutable/update/consume markers, mode inference)
    purpose: Bring the discipline to ordinary Scala including concurrency APIs
    Claimed implementation in the compiler; independent evidence would be shipped compiler sources/tests with hash.

how reviews work

0 comments
Cite this review

Pith. "Pith review of System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)." pith.science (2026). https://pith.science/paper/76Z5AOBP

@misc{pith2026260709383,
  author       = {Pith},
  title        = {Pith review of: System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/76Z5AOBP}},
  note         = {Machine review of arXiv:2607.09383}
}
read the original abstract

Substructural type systems give strong static control over aliasing. Examples include uniqueness, separation, and borrowing. How can such control be brought to established languages whose programming models rely on higher-order abstraction, unrestricted aliasing, and pervasive sharing? We study this problem in the context of Scala. We show how to retrofit these guarantees selectively instead of globally: ordinary code keeps Scala's usual aliasing discipline, while stronger guarantees can be enforced where they matter. Our starting point is Scala's capture checking, whose treatment of capabilities is inspired by the object-capability tradition: capabilities are ordinary values, and capture sets record, in a value's type, which capabilities the value may use. We develop System Capybara, which adds a selective alias-control layer to this mechanism. By tracking separation, consumption, freshness, and read-only access for capabilities, Capybara recovers key reasoning principles from substructural and ownership-based disciplines without global invariants. We give a type-preserving translation from the surface calculus Capybara to CoreCapybara, a core calculus extending System Capless, the earlier foundation for capture checking. The translation uses quantifiers for capture polymorphism and freshness, and constraint-indexed modal types for separation. We prove a semantic soundness result for the core calculus in Lean 4 and derive type safety, memory safety (no use-after-free or double-free), immutability of read-only computations, and data-race freedom for well-typed programs. Finally, we implement Scala 3's new separation checker, which brings higher-order separation reasoning about effects, capabilities, and resources to ordinary Scala, including fearless concurrency.

Figures

Figures reproduced from arXiv: 2607.09383 by the authors.

Figure 1
Figure 1. Abstract syntax of System Capybara. a capture lambda, or a constant. The memory primitives and parallel composition are typed in Section 3.4. The parameter of a term lambda carries a consume mode 𝛼, recording whether the argument may only be accessed (𝜖) or also consumed (consume). Section 3.3 formalizes consume. A capturing type 𝑚 𝑆 ∧ 𝐶 consists of a permission 𝑚 qualifying the type, a shape type 𝑆, and a capture s… view at source ↗
Figure 2
Figure 2. Main typing rules of System Capybara [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Typing rules for capabilities. every element of 𝐶 with the access mode 𝜇: 𝜖 𝐶 = 𝐶 ro𝐶 = {ro𝜃 | 𝜇 𝜃 ∈ 𝐶} consume𝐶 = {consume𝜃 | 𝜇 𝜃 ∈ 𝐶}. (sc-mode) lets a capture set be qualified down to a weaker mode, since ro ⪯ 𝜖; (sc-ro-mono) extends this to a congruence under qualifying. Subbounding. Subbounding Γ ⊢ 𝐵1 <: 𝐵2 extends subcapturing to capture bounds 𝐵. (sb-mode) orders mutability bounds the same way as mutabilities… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: The running example, surface (left) against core (right), aligned construct by construct. [PITH_FULL_IMAGE:figures/full_fig_p013_4.png]
Figure 5
Figure 5. Figure 5: Typing rules for mutable state, parallelism, and conditionals of System Capybara. [PITH_FULL_IMAGE:figures/full_fig_p014_5.png]
Figure 6
Figure 6. Figure 6: Syntax of System CoreCapybara: the delta over Capybara (Figure [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]
Figure 7
Figure 7. Figure 7: The logical model of CoreCapybara: denotations of capture sets, types, and expressions, and the [PITH_FULL_IMAGE:figures/full_fig_p018_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

92 extracted references · 22 canonical work pages

  1. [1]

    2004.Semantics of types for mutable state

    Amal Ahmed. 2004.Semantics of types for mutable state. Princeton University (cit. on pp. 17, 26)

    2004

  2. [2]

    Amal Ahmed. 2006. Step-indexed syntactic logical relations for recursive and quantified types. InESOP(Lecture Notes in Computer Science). Vol. 3924. Springer, 69–83. doi:10.1007/11693024\_6 (cit. on pp. 26, 38)

    work page doi:10.1007/11693024 2006

  3. [3]

    Amal Ahmed, Derek Dreyer, and Andreas Rossberg. 2009. State-dependent representation independence. InPOPL. ACM, 340–353. doi:10.1145/1480881.1480925 (cit. on p. 26)

    doi:10.1145/1480881.1480925 2009

  4. [4]

    Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The essence of dependent object types. InA List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday(Lecture Notes in Computer Science). Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, (Eds.) Vol. ...

    doi:10.1007/978-3-319-30936-1 2016

  5. [5]

    Appel and David A

    Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code.ACM Trans. Program. Lang. Syst., 23, 5, 657–683. doi:10.1145/504709.504712 (cit. on pp. 17, 26)

    doi:10.1145/504709.504712 2001

  6. [6]

    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 pp. 22, 25)

    2023

  7. [7]

    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. 25)

    2016

  8. [8]

    Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bračevac, and Tiark Rompf. 2025. Modeling reachability types with logical relations: Semantic type soundness, termination, effect safety, and equational theory.Proc. ACM Program. Lang., 9, OOPSLA2, 1837–1864. doi:10.1145/3763116 (cit. on pp. 24, 26)

    work page doi:10.1145/3763116 2025

Show all 92 references
  1. [9]

    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 pp. 2, 25)

    1996

  2. [10]

    Newton, Simon L

    Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon L. Peyton Jones, and Arnaud Spiwack. 2018. Linear Haskell: Practical linearity in a higher-order polymorphic language.Proc. ACM Program. Lang., 2, POPL, 5:1–5:29 (cit. on pp. 3, 25)

    2018

  3. [11]

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

  4. [12]

    Capturing types.ACM Trans. Program. Lang. Syst., 45, 4, 21:1–21:52 (cit. on pp. 2–4, 7, 24)

  5. [13]

    Chandrasekhar Boyapati, Robert Lee, and Martin C. Rinard. 2002. Ownership types for safe programming: Preventing data races and deadlocks. InProceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, Seattle,...

    2002 doi

  6. [14]

    John Boyland. 2003. Checking interference with fractional permissions. InStatic Analysis, 10th International Sym- posium, SAS 2003, San Diego, CA, USA, June 11-13, 2003, Proceedings(Lecture Notes in Computer Science). Radhia Cousot, (Ed.) Vol. 2694. Springer, 55–72. doi:10.100...

    2003 doi

  7. [15]

    John Boyland, James Noble, and William Retert. 2001. Capabilities for sharing: A generalisation of uniqueness and read-only. InECOOP(Lecture Notes in Computer Science). Vol. 2072. Springer, 2–27. doi:10.1007/3-540-45337-7\_2 (cit. on p. 25)

    2001 doi

  8. [16]

    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 p. 25)

    2022

  9. [17]

    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 p. 25)

    2020

  10. [18]

    Elias Castegren and Tobias Wrigstad. 2016. Reference capabilities for concurrency control. In30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy(LIPIcs). Shriram Krishnamurthi and Benjamin S. Lerner, (Eds.) Vol. 56. Schloss Dagstu...

    2016 doi

  11. [19]

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

    2013

  12. [20]

    Dave Clarke and Tobias Wrigstad. 2003. External uniqueness is unique enough. InECOOP(Lecture Notes in Computer Science). Vol. 2743. Springer, 176–200 (cit. on pp. 23, 25)

    2003

  13. [21]

    Clarke, John Potter, and James Noble

    David G. Clarke, John Potter, and James Noble. 1998. Ownership types for flexible alias protection. InProceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, OOPSLA 1998, Vancouver, British Columbia, Canada, October 18-2...

    1998 doi

  14. [22]

    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. 25). 28 Xu et al

    2017

  15. [23]

    Aaron Craig, Alex Potanin, Lindsay Groves, and Jonathan Aldrich. 2018. Capabilities: Effects for Free. InFormal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceed...

    2018 doi

  16. [24]

    Gregory Morrisett

    Karl Crary, David Walker, and J. Gregory Morrisett. 1999. Typed memory management in a calculus of capabilities. InPOPL. ACM, 262–275. doi:10.1145/292540.292564 (cit. on p. 25)

    1999 doi

  17. [25]

    Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. InCADE 28 (Lecture Notes in Computer Science). Vol. 12699. Springer, 625–635. doi:10.1007/978-3-030-79876-5\_37 (cit. on pp. 3, 17)

    2021 doi

  18. [26]

    Dennis and Earl C

    Jack B. Dennis and Earl C. Van Horn. 1966. Programming semantics for multiprogrammed computations.Commun. ACM, 9, 3, 143–155. doi:10.1145/365230.365252 (cit. on p. 25)

    1966 doi

  19. [27]

    Vlastimil Dort and Ondrej Lhoták. 2020. Reference mutability for DOT. InECOOP(LIPIcs). Vol. 166. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 18:1–18:28. doi:10.4230/LIPIcs.ECOOP.2020.18 (cit. on p. 25)

    2020 doi

  20. [28]

    Manuel Fähndrich and Robert DeLine. 2002. Adoption and focus: Practical linear types for imperative programming. InPLDI. ACM, 13–24. doi:10.1145/512529.512532 (cit. on p. 25)

    2002 doi

  21. [29]

    Matthew Fluet, Greg Morrisett, and Amal Ahmed. 2006. Linear regions are all you need. InESOP(Lecture Notes in Computer Science). Vol. 3924. Springer, 7–21 (cit. on p. 25)

    2006

  22. [30]

    Foster, Manuel Fähndrich, and Alexander Aiken

    Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. 1999. A theory of type qualifiers. InPLDI. ACM, 192–203 (cit. on p. 25)

    1999

  23. [31]

    Foster, Robert Johnson, John Kodumal, and Alex Aiken

    Jeffrey S. Foster, Robert Johnson, John Kodumal, and Alex Aiken. 2006. Flow-insensitive type qualifiers.ACM Transactions on Programming Languages and Systems, 28, 6, (Nov. 2006), 1035–1087. doi:10.1145/1186632.1186635 (cit. on p. 25)

    2006 doi

  24. [32]

    Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer

    Aïna Linn Georges, Benjamin Peters, Laila Elbeheiry, Leo White, Stephen Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer. 2025. Data race freedom à la mode.Proc. ACM Program. Lang., 9, POPL, 656–686. doi:10.1145/3704859 (cit. on pp. 3, 25)

    2025 doi

  25. [33]

    Jean-Yves Girard. 1987. Linear logic.Theoretical Computer Science, 50, 1–102. doi:10.1016/0304-3975(87)90045-4 (cit. on p. 25)

    1987 doi

  26. [34]

    Colin S. Gordon. 2020. Designing with static capabilities and effects: Use, mention, and invariants (pearl). In34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference)(LIPIcs). Robert Hirschfeld and Tobias ...

    2020 doi

  27. [35]

    Gordon, Matthew J

    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. 2012. Uniqueness and reference immutability for safe parallelism. InOOPSLA. ACM, 21–40. doi:10.1145/2384616.2384619 (cit. on p. 25)

    2012 doi

  28. [36]

    Michael Gottesman and Joe Groff. 2023. SE-0377: borrowing and consuming parameter ownership modifiers. https ://github.com/swiftlang/swift-evolution/blob/main/proposals/0377-parameter-ownership-modifiers.md. Swift Evolution proposal; implemented in Swift 5.9. Accessed: 2026-07...

    2023

  29. [37]

    Joe Groff, Michael Gottesman, Andrew Trick, and Kavon Farvardin. 2023. SE-0390: Noncopyable structs and enums. https://github.com/swiftlang/swift-evolution/blob/main/proposals/0390-noncopyable-structs-and-enums.md. Swift Evolution proposal; implemented in Swift 5.9. Accessed: ...

    2023

  30. [38]

    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. InPLDI. ACM, 282–293 (cit. on p. 25)

    2002

  31. [39]

    Philipp Haller and Alexander Loiko. 2016. LaCasa: Lightweight affinity and object capabilities in Scala. InProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amste...

    2016 doi

  32. [40]

    Philipp Haller and Martin Odersky. 2010. Capabilities for uniqueness and borrowing. InECOOP 2010 – Object-Oriented Programming. Theo D’Hondt, (Ed.) Springer, Berlin, Heidelberg, 354–378.isbn: 978-3-642-14107-2. doi:10.1007/978-3 -642-14107-2_17 (cit. on p. 25)

    2010 doi

  33. [41]

    John Hogg. 1991. Islands: Aliasing protection in object-oriented languages. InProceedings of the Sixth Annual Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 1991, Phoenix, Arizona, USA, October 6-11, 1991. Andreas Paepcke, (Ed.) ACM, 271...

    1991 doi

  34. [42]

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2021. Safe systems programming in Rust. Commun. ACM, 64, 4, 144–152. doi:10.1145/3418295 (cit. on pp. 1, 25)

    2021 doi

  35. [43]

    Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic.J. Funct. Program., 28, e20. doi:10.1017/S0956796818000151 (cit. on pp. 25, 26). S...

    2018 doi

  36. [44]

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. InPOPL. ACM, 637–650. doi:10.1145/2 676726.2676980 (cit. on p. 26)

    2015 doi

  37. [45]

    Steve Klabnik and Carol Nichols. 2024. Fearless concurrency. Chapter 16, The Rust Programming Language. Accessed: 2026-06-20. https://doc.rust-lang.org/book/ch16-00-concurrency.html (cit. on p. 1)

    2024

  38. [46]

    2019.The Rust programming language

    Steve Klabnik and Carol Nichols. 2019.The Rust programming language. No Starch Press (cit. on pp. 1, 2, 25)

    2019

  39. [47]

    Edward Lee and Ondrej Lhoták. 2023. Simple Reference Immutability for System F.Proc. ACM Program. Lang., 7, OOPSLA2, 857–881. doi:10.1145/3622828 (cit. on p. 25)

    2023 doi

  40. [48]

    Daan Leijen. 2014. Koka: Programming with row polymorphic effect types. InMSFP 2014, 100–126. doi:10.4204 /EPTCS.153.8 (cit. on p. 25)

    2014

  41. [49]

    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 pp. 3, 25)

    2024

  42. [50]

    Lucassen and David K

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

    1988

  43. [51]

    Danielle Marshall and Dominic Orchard. 2024. Functional ownership through fractional uniqueness.Proc. ACM Program. Lang., 8, OOPSLA1, 1040–1070. doi:10.1145/3649848 (cit. on p. 25)

    2024 doi

  44. [52]

    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 pp. 2, 25)

    2022

  45. [53]

    Matsakis and Felix S

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

    2014

  46. [54]

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

    2017

  47. [55]

    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

  48. [56]

    Mae Milano, Joshua Turcotti, and Andrew C. Myers. 2022. A flexible type system for fearless concurrency. InPLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022. Ranjit Jhala and Isil Dilli...

    2022 doi

  49. [57]

    Heather Miller, Philipp Haller, and Martin Odersky. 2014. Spores: A type-based foundation for closures in the age of concurrency and distribution. InECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings(Lect...

    2014 doi

  50. [58]

    Mark S. Miller. 2006.Robust composition: Towards a unified approach to access control and concurrency control. Ph.D. Dissertation. John Hopkins University (cit. on p. 25)

    2006

  51. [59]

    Modular. 2026. Mojo manual: Ownership. https : / / mojolang . org / docs / manual / values / ownership/. Accessed: 2026-07-06. (2026) (cit. on pp. 3, 25)

    2026

  52. [60]

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

    2008

  53. [61]

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

    1998

  54. [62]

    Peter W. O’Hearn. 2003. On bunched typing.J. Funct. Program., 13, 4, 747–796 (cit. on p. 25)

    2003

  55. [63]

    O’Hearn, John Power, Makoto Takeyama, and Robert D

    Peter W. O’Hearn, John Power, Makoto Takeyama, and Robert D. Tennent. 1999. Syntactic control of interference revisited.Theor. Comput. Sci., 228, 1-2, 211–252. doi:10.1016/S0304-3975(98)00359-4 (cit. on p. 25)

    1999 doi

  56. [64]

    O’Hearn, John C

    Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. InComputer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings(Lectu...

    2001 doi

  57. [65]

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

  58. [66]

    InSCALA/SPLASH

    Safer exceptions for Scala. InSCALA/SPLASH. ACM, 1–11 (cit. on p. 24)

  59. [67]

    Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. 2019. Quantitative program reasoning with graded modal types.Proc. ACM Program. Lang., 3, ICFP, 110:1–110:30. doi:10.1145/3341714 (cit. on p. 25)

    2019 doi

  60. [68]

    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. InOOPSLA. ACM, 234–251 (cit. on p. 25)

    2016

  61. [69]

    Leo Osvald and Tiark Rompf. 2017. Rust-like borrowing with 2nd-class values (short paper). InSCALA@SPLASH. ACM, 13–17. doi:10.1145/3136000.3136010 (cit. on p. 25)

    2017 doi

  62. [70]

    [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 pp. 22, 25). 30 Xu et al

    2024

  63. [71]

    Reynolds

    John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. InLICS. IEEE Computer Society, 55–74 (cit. on p. 25)

    2002

  64. [72]

    Reynolds

    John C. Reynolds. 1989. Syntactic control of inference, part 2. InAutomata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings(Lecture Notes in Computer Science). Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and...

    1989 doi

  65. [73]

    Reynolds

    John C. Reynolds. 1978. Syntactic control of interference. InPOPL. ACM Press, 39–46 (cit. on p. 25)

    1978

  66. [74]

    Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). InOOPSLA. ACM, 624–641 (cit. on p. 24)

    2016

  67. [75]

    Capture checker,

    [SW Mod.] Scala, “Capture checker, ” part of Scala 3 2024 EPFL LAMP.url: https://nightly.scala-lang.org/docs/refer ence/experimental/capture-checking/index.html,vcs: https://github.com/scala/scala3 (cit. on p. 24)

    2024

  68. [76]

    [SW Mod.] Scala, Separation checking 2026 EPFL LAMP.url: https://nightly.scala-lang.org/docs/reference/experim ental/capture-checking/separation-checking.html,vcs: https://github.com/scala/scala3 (cit. on p. 24)

    2026

  69. [77]

    Jan Smans, Bart Jacobs, and Frank Piessens. 2009. Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. InECOOP(Lecture Notes in Computer Science). Vol. 5653. Springer, 148–172. doi:10.1007/978-3-64 2-03013-0_8 (cit. on p. 26)

    2009 doi

  70. [78]

    Jean-Pierre Talpin and Pierre Jouvelot. 1992. Polymorphic type, region and effect inference.Journal of Functional Programming, 2, 3, 245–271 (cit. on p. 25)

    1992

  71. [79]

    Wenhao Tang and Sam Lindley. 2026. Rows and capabilities as modal effects.Proc. ACM Program. Lang., 10, POPL, 923–950. doi:10.1145/3776674 (cit. on p. 25)

    2026 doi

  72. [80]

    Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, and Anton Lorenzen. 2025. Modal effect types.Proc. ACM Program. Lang., 9, OOPSLA1, 1130–1157. doi:10.1145/3720476 (cit. on pp. 3, 25)

    2025 doi

  73. [81]

    Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2024. A logical approach to type soundness.J. ACM, 71, 6, 40:1–40:75. doi:10.1145/3676954 (cit. on pp. 3, 17, 26, 38)

    2024 doi

  74. [82]

    Mads Tofte and Jean-Pierre Talpin. 1994. Implementation of the typed call-by-value lambda-calculus using a stack of regions. InPOPL. ACM Press, 188–201 (cit. on p. 25)

    1994

  75. [83]

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

    1997

  76. [84]

    Tschantz and Michael D

    Matthew S. Tschantz and Michael D. Ernst. 2005. Javari: Adding reference immutability to Java. InOOPSLA. ACM, 211–230. doi:10.1145/1094811.1094828 (cit. on p. 25)

    2005 doi

  77. [85]

    Philip Wadler. 1990. Linear types can change the world! InProgramming Concepts and Methods. North-Holland, 561 (cit. on pp. 2, 25)

    1990

  78. [86]

    Gregory Morrisett

    David Walker, Karl Crary, and J. Gregory Morrisett. 2000. Typed memory management via static capabilities.ACM Trans. Program. Lang. Syst., 22, 4, 701–771. doi:10.1145/363911.363923 (cit. on p. 25)

    2000 doi

  79. [87]

    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. 24)

    2024

  80. [88]

    Matsakis, and Amal Ahmed

    Aaron Weiss, Olek Gierczak, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2020. Oxide: The essence of Rust.arXiv:1903.00982 [cs], (Aug. 2020). arXiv: 1903.00982[cs](cit. on p. 25)

    2020 arXiv

  81. [89]

    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. InECOOP(LIPIcs). Vol. 222. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 15:1–15:29 (cit. on p. 25)

    2022

  82. [90]

    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. 24)

    2024 doi

  83. [91]

    Yichen Xu, Oliver Bračevac, Cao Nguyen Pham, and Martin Odersky. 2025. What’s in the box: Ergonomic and expressive capture tracking over generic data structures.Proc. ACM Program. Lang., 9, OOPSLA2, 1726–1753. doi:10.1145/3763112 (cit. on pp. 2–4, 14, 24)

    2025 doi

  84. [92]

    separate

    Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer. 2021. GhostCell: Separating permissions from data in Rust.Proc. ACM Program. Lang., 5, ICFP, 1–30. doi:10.1145/3473597 (cit. on p. 25). System Capybara: Tracking Capabilities for Separation and Freshness 31 A Comple...

    2021 doi

Pith tools

Reviewed July 13, 2026 · model on record in the stance chip above.