Pith. sign in

REVIEW 2 major objections 7 minor 66 references

Classifying Capabilities (Extended Version)

T0 review · 2 major / 7 minor · reviewed 2026-07-31 · grok-4.5

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

Pith's one-line read Capability classifiers let capture checking filter effects by kind, not just by identity, so Scala’s Try and Future finally type-check precisely.

desk verdict Solid systems+theory package that actually unblocks capture-checked Try/Future; the Lean core is real, the tree design is a conscious tradeoff, and the only practical gap is an unverified hand-port of the kind algebra into the Scala checker. read the letter →

arxiv 2607.24504 v1 pith:JKANV6SJ submitted 2026-07-27 cs.PL

Cao Nguyen Pham (1) , Oliver Bračevac (1) , Yichen Xu (1) , Yaoyu Zhao (1) , Martin Odersky (1) ((1) EPFL) This is my paper
classification cs.PL
keywords capturecheckingcapabilityclassifierseffectexclusionScala3SystemCaplesskindalgebraexceptioninterceptiontypesafety
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

Capture checking already tracks which values a piece of code may hold, but it cannot say “only the control-flow ones” or “none of the thread-local ones.” That gap kept Try and Future, and many real exclusion patterns, outside the checked standard library. This paper adds capability classifiers: an open tree of semantic tags on capabilities, with projections that keep only a subtree or drop a subtree from a capture set. Separate branches stay disjoint even when other modules later extend the tree, which fits separate compilation. The design is formalized as System Capless(K), proved safe under a checked big-step semantics (type safety, effect safety, capture prediction, handler coverage) and fully mechanized in Lean 4, then implemented in the Scala 3 capture checker and used on library APIs and replicated exclusion case studies.

What carries the argument

Classifier kinds as holed subtrees (a root with excluded child subtrees), with algorithmic intersection, subtraction, emptiness, subkinding, and disjointness; projected captures (θ|ϕ) and C.proj[ϕ] that filter capture sets; plus intercept for classifier-indexed exception handling in the operational model.

What would settle it

Find a standard-library or production API whose needed exclusion or privilege split cannot be written with tree classifiers and only/except (for example requiring a non-empty meet of sibling kinds, or true multi-tag classification), or exhibit a well-typed Capless(K) term that gets stuck or leaks a label outside its predicted use set under the checked evaluator.

Watch

Extended reading notes

Core claim

A tree-structured, user-extensible hierarchy of capability classifiers, together with only/except projections on capture sets and a decidable kind algebra of subtree intersection, union, and subtraction, is enough to state kind-level inclusion and exclusion constraints that capture checking previously could not express, while remaining modular under separate compilation and type-safe under a mechanized big-step semantics.

Load-bearing premise

Capabilities must live in a single-inheritance open tree so sibling branches stay forever disjoint; if a real taxonomy needs one capability to sit under two sibling kinds at once, the algebra and the compiler’s dual-parent ban break down.

Editorial extensions

If this is right

  • Try can be typed as retaining only the body’s Control captures, and Future as forbidding ThreadLocal (hence Control) captures.
  • Open effect-exclusion patterns previously stated with boolean effect algebras can be expressed per-reference via projections on concrete capture paths.
  • Capture-checked standard-library coverage rises once Try, Future, and related packages become precisely typable.
  • Handler coverage and used-label prediction become static consequences of kind annotations on intercept and use sets.

Reading between the lines

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

  • Libraries that today over-approximate with any or under-approximate with purity may migrate to kind-filtered signatures without abandoning capture checking.
  • The missing kind variables and non-trivial sibling meets point to a natural next calculus that would combine tree complements with limited kind polymorphism or separation checking.
  • Encoding serializability or unscoped-return restrictions as classifier traits suggests classifiers can absorb several ad-hoc closure DSLs into ordinary capture sets.
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

2 major / 7 minor

Summary. The paper introduces capability classifiers for Scala 3 capture checking: a tree-structured, user-extensible hierarchy of tags with projections (c.only[C], c.except[C]) that filter capture sets by classifier kind. The authors formalize this as System Capless(K), an extension of System Capless, with a kind algebra of holed subtrees (union/intersection/subtraction), a checked big-step operational semantics extended with boundary/break and a new intercept construct, and prove type safety, effect safety, used-label prediction, capture prediction, and handler coverage (Theorem 4.1 / A.5–A.6, Corollaries 4.2–4.6 / A.7–A.13), all mechanized in ~10k lines of Lean 4 with no sorries and no axioms beyond the kernel. The design is implemented in the Scala 3 capture checker; the paper reports standard-library coverage rising to 81.7%, gives precise classifier-based signatures for Try and Future, replicates all 59 Flix effect-exclusion case studies, and includes a mechanized Church encoding of Try (Appendix B.9).

Significance. If the results hold, this is a solid contribution at the intersection of effect systems and capability-based reasoning. The central problem — expressing "only the control-flow part of this closure" or "exclude thread-local capabilities" — is well motivated by concrete standard-library types (Try, Future) that previously had to be typed imprecisely or left outside capture checking. The design point (an open tree rather than a lattice, so that disjointness is stable under separate compilation) is argued carefully in §6.1 with honest comparison to Flix's boolean-algebraic approach and InvalML. Three strengths deserve explicit credit: (1) the metatheory is fully mechanized in Lean 4, with unusually transparent rule/theorem correspondence tables (Tables 3–4, Appendix B.8) and a candid list of representation differences from the paper presentation (Appendix B.7); (2) the big-step account is a genuine methodological contribution over prior syntactic progress/preservation proofs in this line, enabling capture prediction and handler coverage statements that a small-step proof would not give directly; (3) the system is not just a calculus — it ships in the Scala 3 compiler, is exercised on 5

major comments (2)
  1. [§5, Declaring Classifiers; §3.1] Every disjointness-dependent result — the kind algebra's (i-disjoint)/(st-*) rules, the set-semantics justification (§4.1), the soundness of .except projections, and hence the Try/Future signatures — rests on the sub-classifier-or-disjoint tree invariant of §3.1. In the Lean development this is part of the formal setup and machine-checked. But the paper also claims (abstract, §5) that the design is implemented in the Scala 3 capture checker, where the invariant is maintained only by an unverified compiler check rejecting dual classifier inheritance. The check is described in one sentence ('the compiler rejects any class that inherits two unrelated classifier traits') without defining 'unrelated': does a diamond through a shared classifier ancestor count? What about a classifier trait mixed into another classifier trait, or Java interfaces? Since this check is the entire trusted base conn
  2. [§4.3, Theorem 4.1; Abstract] Theorem 4.1 is stated with Σ ⊢ t ⇓?_F a, i.e., evaluation 'terminates with answer a or gets stuck', so the theorem is conditional on non-divergence: 'evaluation does not get stuck' is proved only for runs that do not diverge. The abstract and §4.3 paraphrase this as 'well-typed terms do not get stuck', which is strictly stronger than the mechanized statement. The calculus as presented has no recursion or general fixpoint primitive, so strong normalization is plausible and the caveat may be vacuous in practice — but it is unproved, and §6.5/future-work discussions suggest extensions that would add recursion. One or two sentences at Theorem 4.1 (and a matching hedge in the abstract/intro) should state the non-divergence condition explicitly and say whether strong normalization holds, is conjectured, or is out of scope. This is standard for big-step accounts but should not be left implicit
minor comments (7)
  1. [§5, Standard-Library Coverage] The two line counts use different denominators (54,992 vs 54,841 lines) for the with-classifiers and baseline versions. A sentence explaining the difference (added library code? different tokei version?) would make the 66.7% → 81.7% comparison easier to interpret. It would also help to state what fraction of the newly covered lines is in scala.util/scala.concurrent, i.e., the portion directly attributable to classifiers versus the 'accompanying library changes'.
  2. [§4.2, Fig. A.3 (rt-app)] In (rt-app) the symbol C1 is used both as the use set of the function sub-term and as the capture set of its function type (∀(z : S∧C0)E)∧C1. The accompanying prose explains the intended alignment invariant, but the shared metavariable is confusing on first read; consider renaming one occurrence or adding an explicit side condition.
  3. [§4.3, Corollary 4.6(2); §A.5] Corollary 4.6(2) is flagged as 'trivial from the evaluation rules' in Appendix A.5 but presented alongside the non-trivial Breaks clause in the main text. The candid footnote is appreciated; consider moving the qualifier into the main text so readers calibrate the corollary's content correctly.
  4. [Appendix B.10] The Lean development is described as ~10k lines in 59 files building with Lean 4.30.0, but no repository URL or artifact DOI is given anywhere in the manuscript. Please add a stable link (or an anonymized artifact reference if under double-blind review).
  5. [§6.2, first paragraph] Typo: 'succesfully' → 'successfully'.
  6. [Fig. 5 / Fig. A.2, Exclusive Union; Fig. 4 (abs)] The 'exclusive union' C ⊎ {x1,...,xn} requires ∀i,φ.(xi|φ) ∉ C, but (abs) and (rt-abs) use C ⊎ {x} without restating this side condition; since Γ already binds x, the condition presumably follows from well-formedness of contexts — worth a one-line remark for readers checking the figures standalone.
  7. [Fig. 7, Handler type abbreviations] The Handler_pass/Handler_gen abbreviations quantify ∀[c : Ct.proj[φ]] over a capture variable bounded by a projected capture set, but Ct is a metavariable over sets, not a context element; readers must infer that Ct is substituted by a closed set before the bound is well-formed. A sentence clarifying that these are schema-level abbreviations would help.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: safety and kind-algebra results are independently mechanized, not fitted or definitionally forced renamings of the inputs.

full rationale

System Capless(K) extends prior capture-checking work (System Capless) with classifier kinds, projections, and intercept, then re-establishes type/effect safety, capture prediction, and handler coverage via a checked big-step semantics fully mechanized in Lean 4 without sorries. That is ordinary cumulative PL work: the prior calculus is infrastructure, not a uniqueness theorem that forces the present theorems, and the main claims are proved from the stated rules rather than recovered by construction from fitted parameters or tautological renamings. The tree-shaped classifier universe is an explicit design choice that makes branch disjointness stable under open extension; disjointness is not smuggled in as a predicted empirical law. Standard-library coverage figures and Flix case-study replications are post-hoc measurements of the implementation, not inputs to the metatheory. No self-definitional loop, fitted-input-as-prediction, or load-bearing unverified self-citation chain appears in the derivation of Theorem 4.1 or Corollaries 4.2–4.6.

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

This is a type-systems paper: load-bearing content is definitions plus theorems, not fitted constants. Background rests on standard type-theoretic practice and the prior capture-checking stack. The main invented structure is the classifier-kind universe and its tree discipline chosen for modular disjointness.

assumptions (4)
  • standard math Standard type-safety metatheory for a lambda calculus with subtyping, existential capture packs, and substitution-based big-step evaluation (progress/safety via induction on evaluation).
    Used throughout Sections 3–4 and Appendix A; Lean kernel trusts only standard foundations.
  • domain assumption Prior System Capless / capture-checking account of capturing types, use sets vs capture sets, and surface any-desugaring (Xu et al., Boruch-Gruszecki et al.).
    Capless(K) is explicitly an extension; MNF embedding and library integration assume that stack.
  • ad hoc to paper Classifier universe is an open tree embeddable in an infinite tree: unique parent paths, countably infinite children per node, dual classifier inheritance forbidden so sub-classifier-or-disjoint holds.
    Section 3.1 and 6.1; this is the design axiom that buys decidable modular disjointness and shapes the kind algebra.
  • domain assumption Operational model of exceptions via boundary/break plus intercept on classifier-filtered labels adequately represents Scala/JVM intercepting handlers and Try for the stated safety theorems.
    Sections 3.6–3.7 and 6.4; theorems are about this model, not a full JVM exception semantics.
invented entities (2)
  • Capability classifiers and classifier kinds (holed subtrees with union/intersection/subtraction) independent evidence
    purpose: Tag capabilities by semantic role and filter capture sets via only/except projections.
    Core contribution; realized as Scala traits and as Kind algebra in Capless(K).
  • intercept control operator with pass/gen handler typings independent evidence
    purpose: Model intercepting exception handlers and prove handler coverage / refined use sets.
    Section 3.7; bridges lexical boundaries and non-lexical catch for Try encoding.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Classifying Capabilities (Extended Version)." pith.science (2026). https://pith.science/paper/JKANV6SJ

@misc{pith2026260724504,
  author       = {Pith},
  title        = {Pith review of: Classifying Capabilities (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JKANV6SJ}},
  note         = {Machine review of arXiv:2607.24504}
}
read the original abstract

Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as "retaining only the control-flow capabilities of this closure" or "excluding all thread-local capabilities from this argument" become inexpressible. Both arise in the Scala 3 standard library: "Try" re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and "Future" must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion ("c.only[C]") and exclusion ("c.except[C]"). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns.

Figures

Figures reproduced from arXiv: 2607.24504 by the authors.

Figure 1
Figure 1. Classifiers in Scala: declarations (left) and excluding the [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Try[T] signatures before classifiers (left) and with classifiers (right). 2.2 Case Study: Try[T] Captures Control Capabilities Try[T] [42] is a sum type representing either a successful value or an arbitrary runtime exception, enabling fluid conversion between exception-based and monadic error handling. Under previous capture checking, the constructor and re-throwing accessor had the signatures in [PITH_FULL_IMAGE:… view at source ↗
Figure 3
Figure 3. Abstract syntax of System Capless(K). Changes compared to System Capless [59] are marked . which pair a shape type with a capture set. Existential types ∃𝑐.𝑇 allow existentially quantifying a capture set, enabling abstraction over unknown capabilities. The calculus supports three forms of polymorphism: term abstraction over values, type abstraction over type variables bounded by shape types, and capture abstraction … view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Type system of System Capless(K) (condensed). Changes compared to System Capless [59] are marked . The complete type system is given in Figure A.1 [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Kind algebra of System Capless(K) (condensed). The complete kind algebra is given in Figure A.2. Each node has a countably infinite number of children. This is crucial for modularity, as a classifier cannot be “singled out” by excluding all its known sub-classifiers: a…
Figure 6
Figure 6. Figure 6: Checked big-step semantics of System Capless( [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]
Figure 7
Figure 7. Figure 7: Extended System Capless(K) with boundaries and interceptions. also reasons in big-step style about what function values may capture, and logical-relations work on reachability types [3], which connects annotations to the values reachable at runtime. Neither qualifies t…
Figure 8
Figure 8. Figure 8: Checked big-step semantics of System Capless( [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]
Figure 9
Figure 9. Figure 9: Capture Kinding for Labels, Relaxed typing definitions (selected rules) and Answer Typing rules used [PITH_FULL_IMAGE:figures/full_fig_p015_9.png]
Figure 10
Figure 10. Figure 10: The kind remainder computation, abridged. Com [PITH_FULL_IMAGE:figures/full_fig_p018_10.png]
Figure 11
Figure 11. Figure 11: Effect exclusion in real-world APIs: RunWithErrHandler from dune (left) and withTransaction from google-cloud-go (right). is not possible to assert that db.readUsers uses db.only[UserTable] and not db.only[TransactionTable]. trait Database extends Classifier, Exclusiv…
Figure 12
Figure 12. Figure 12: Read-only parallel map: (a) capability declarations, (b) their use, and (c) encapsulating the capability [PITH_FULL_IMAGE:figures/full_fig_p021_12.png]
Figure 13
Figure 13. Figure 13: Intercepting handlers: logErrors rethrows the caught exception (left), captureException stores it together with its CanThrow capability (right). When type-checking the closure passed into parMap, the presence of the file.rw capability causes the compiler to reject the…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

66 extracted references · 18 canonical work pages

  1. [1]

    Anonymous. 2026. System Capybara: tracking capabilities for separation and freshness. Under submission. (2026) (cit. on pp. 19, 23, 24)

    2026

  2. [2]

    Error handling,

    [SW Mod.] Apple Inc., “Error handling, ” part of Swift 2015Apple Inc.url: https://docs.swift.org/swift-book/docume ntation/the-swift-programming-language/errorhandling/,vcs: https://github.com/swiftlang/swift (cit. on p. 25)

  3. [3]

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

    doi:10.1145/3763116 2025

  4. [4]

    Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers.J. Log. Algebraic Methods Program., 84, 1, 108–123. doi:10.1016/J.JLAMP.2014.02.001 (cit. on pp. 24, 25)

    doi:10.1016/j.jlamp.2014.02.001 2015

  5. [5]

    Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. 2018. Handle with care: Relational interpre- tation of algebraic effects and handlers.Proc. ACM Program. Lang., 2, POPL, 8:1–8:30. doi:10.1145/3158096 (cit. on p. 24)

    work page doi:10.1145/3158096 2018

  6. [6]

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

  7. [7]

    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.1007/3-540-44898-5_4 (cit. on p. 25)

    doi:10.1007/3-540-44898-5_4 2003

  8. [8]

    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. doi:10.1145/3428194 (cit. on pp. 23, 25)

    doi:10.1145/3428194 2020

Show all 66 references
  1. [9]

    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

  2. [10]

    Cunyuan Gao and Lionel Parreaux. 2025. A lightweight type-and-effect system for invalidation safety: Tracking permanent and temporary invalidation with constraint-based subtype inference.Proc. ACM Program. Lang., 9, OOPSLA2, 2623–2653. doi:10.1145/3763144 (cit. on pp. 2, 19, 2...

    2025 doi

  3. [11]

    Goodenough

    John B. Goodenough. 1975. Exception handling: Issues and a proposed notation.Commun. ACM, 18, 12, 683–696. doi:10.1145/361227.361230 (cit. on p. 25)

    1975

  4. [12]

    Gordon, Matthew J

    Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. 2012. Uniqueness and reference immutability for safe parallelism. InProceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications,...

    2012

  5. [13]

    Joy, and Guy L

    James Gosling, William N. Joy, and Guy L. Steele Jr. 1996.The Java Language Specification. Addison-Wesley.isbn: 0-201-63451-1 (cit. on p. 25)

    1996

  6. [14]

    Philipp Haller and Martin Odersky. 2010. Capabilities for uniqueness and borrowing. InECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings(Lecture Notes in Computer Science). Theo D’Hondt, (Ed.) Vol. 6183. Springe...

    2010 doi

  7. [15]

    John Hatcliff and Olivier Danvy. 1994. A generic account of continuation-passing styles. InProceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 458–471. doi:10.1145/174675.178053 (cit. on p. 5)

    1994

  8. [16]

    Young Bae Jun, Hee Sik Kim, and Eun Hwan Roh. 2004. Ideal theory of subtraction algebras.Sci. Math. Jpn. Online, e-2004, 397–402. https://www.jams.jp/scm/contents/e-2004-4/2004-37.pdf (cit. on p. 10)

    2004

  9. [17]

    Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in action! InICFP 2013, 145–158. doi:10.1145/2500365 .2500590 (cit. on p. 25)

    2013 doi

  10. [18]

    James Koppel, Gabriel Scherer, and Armando Solar-Lezama. 2018. Capturing the future by replaying the past (functional pearl).Proc. ACM Program. Lang., 2, ICFP, 76:1–76:29. doi:10.1145/3236771 (cit. on p. 25)

    2018 doi

  11. [19]

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

  12. [20]

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

    2014

  13. [22]

    Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do be do be do. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. Giuseppe Castagna and Andrew D. Gordon, (Eds.) ACM, 500–514. doi:10.11...

    2017

  14. [23]

    Lucassen and David K

    John M. Lucassen and David K. Gifford. 1988. Polymorphic effect systems. InConference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988. Jeanne Ferrante and Peter Mager, (Eds.) ACM Press, 47–57....

    1988

  15. [24]

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

    2024 doi

  16. [25]

    Matthew Lutze, Magnus Madsen, Philipp Schuster, and Jonathan Immanuel Brachthäuser. 2023. With or without you: Programming with effect exclusion.Proc. ACM Program. Lang., 7, ICFP, 448–475. doi:10.1145/3607846 (cit. on pp. 2, 5, 8, 19–21, 23, 24)

    2023 doi

  17. [26]

    Cong Ma, Zhaoyi Ge, Edward Lee, and Yizhou Zhang. 2024. Lexical effect handlers, directly.Proc. ACM Program. Lang., 8, OOPSLA2, 1670–1698. doi:10.1145/3689770 (cit. on p. 25)

    2024 doi

  18. [27]

    Magnus Madsen and Jaco van de Pol. 2020. Polymorphic types and effects with boolean unification.Proc. ACM Program. Lang., 4, OOPSLA, 154:1–154:29. doi:10.1145/3428222 (cit. on p. 24)

    2020 doi

  19. [28]

    Millstein

    Daniel Marino and Todd D. Millstein. 2009. A generic type-and-effect system. InProceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24,

    2009

  20. [29]

    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

  21. [30]

    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

  22. [31]

    2025.Lexical Delimited Continuations for Scala 3

    Guillem Bartrina I Moreno. 2025.Lexical Delimited Continuations for Scala 3. Master’s thesis. EPFL. https://infoscienc e.epfl.ch/entities/publication/5b745359-7d14-4553-a3da-8590f573911c (cit. on p. 25). Master’s thesis

    2025

  23. [32]

    Garrett Morris and James McKinna

    J. Garrett Morris and James McKinna. 2019. Abstracting extensible data types: or, rows by any other name.Proc. ACM Program. Lang., 3, POPL, 12:1–12:28. doi:10.1145/3290325 (cit. on p. 24)

    2019 doi

  24. [33]

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

  25. [34]

    Martin Odersky, Yaoyu Zhao, Yichen Xu, Oliver Bračevac, and Cao Nguyen Pham. 2026. Securing agents with tracked capabilities. InCAIS. ACM, 812–838 (cit. on p. 24)

    2026

  26. [35]

    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. InProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, System...

    2016

  27. [36]

    Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2014. Coeffects: A calculus of context-dependent computation. InICFP 2014, 123–135. doi:10.1145/2628136.2628160 (cit. on p. 23)

    2014

  28. [37]

    Nguyên Cao Pham and Martin Odersky. 2024. Stack-copying delimited continuations for Scala Native. InICOOOLPS. ACM. doi:10.1145/3679005.3685979 (cit. on p. 25)

    2024

  29. [38]

    Plotkin and Matija Pretnar

    Gordon D. Plotkin and Matija Pretnar. 2013. Handling algebraic effects.Log. Methods Comput. Sci., 9, 4. doi:10.2168 /LMCS-9(4:23)2013 (cit. on p. 25)

    2013

  30. [39]

    Didier Rémy. 1989. Typechecking records and variants in a natural extension of ML. InConference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989. ACM Press, 77–88. doi:10.1145/75277.75284 (cit. on p. 24)

    1989

  31. [40]

    2014.A Practical Effect System for Scala

    Lukas Rytz. 2014.A Practical Effect System for Scala. Ph.D. Dissertation. EPFL, Lausanne, Switzerland. doi:10.5075/ep fl-thesis-5935 (cit. on p. 25). 28 Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, and Martin Odersky

    2014 doi

  32. [41]

    Lukas Rytz, Martin Odersky, and Philipp Haller. 2012. Lightweight polymorphic effects. InECOOP 2012 - Object- Oriented Programming - 26th European Conference, Beijing, China, June 11-16, 2012. Proceedings(Lecture Notes in Computer Science). James Noble, (Ed.) Vol. 7313. Spring...

    2012 doi

  33. [42]

    Try API,

    [SW Mod.] Scala, “Try API, ” part of Scala 3 2026EPFL LAMP.url: https://nightly.scala-lang.org/api/scala/util/Try.ht ml,vcs: https://github.com/scala/scala3 (cit. on pp. 1, 5, 13)

  34. [43]

    Capture checker,

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

  35. [44]

    CanThrow API,

    [SW Mod.] Scala, “CanThrow API, ” part of Scala 3 2026EPFL LAMP.url: https://nightly.scala-lang.org/api/scala/Ca nThrow.html,vcs: https://github.com/scala/scala3 (cit. on pp. 4, 5)

  36. [45]

    boundary API,

    [SW Mod.] Scala, “boundary API, ” part of Scala 3 2026EPFL LAMP.url: https://nightly.scala-lang.org/api/scala/util /boundary$.html,vcs: https://github.com/scala/scala3 (cit. on pp. 5, 13)

  37. [46]

    Future API,

    [SW Mod.] Scala, “Future API, ” part of Scala 3 2026EPFL LAMP.url: https://nightly.scala-lang.org/api/scala/concur rent/Future.html,vcs: https://github.com/scala/scala3 (cit. on p. 5)

  38. [47]

    Separation checking,

    [SW Mod.] Scala, “Separation checking, ” part of Scala 3 2026EPFL LAMP.url: https://nightly.scala-lang.org/docs/ref erence/experimental/capture-checking/separation-checking.html,vcs: https://github.com/scala/scala3 (cit. on p. 23)

  39. [48]

    Boris M. Schein. 1992. Difference semigroups.Communications in Algebra, 20, 8, 2153–2169. doi:10.1080/00927879208 824453 (cit. on p. 10)

    1992 doi

  40. [49]

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

    2026 doi

  41. [50]

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

    2025 doi

  42. [51]

    Yan Mei Tang and Pierre Jouvelot. 1995. Effect systems with subtyping. InProceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, La Jolla, California, USA, June 21-23, 1995. Neil D. Jones, (Ed.) ACM Press, 45–53. doi:10.1145/215...

    1995

  43. [52]

    Peter Thiemann. 2025. What I always wanted to know about second class values. InProceedings of the Workshop Dedicated to Olivier Danvy on the Occasion of His 64th Birthday (OLIVIERFEST’25), 117–127. doi:10.1145/3759427.3760 373 (cit. on p. 13)

    2025

  44. [53]

    Peyton Jones

    Keith Wansbrough and Simon L. Peyton Jones. 1999. Once upon a polymorphic type. InPOPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999. Andrew W. Appel and Alex Aiken, (Eds.) ACM, 15–28...

    1999

  45. [54]

    Nicolas Wu, Tom Schrijvers, and Ralf Hinze. 2014. Effect handlers in scope. InProceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014. Wouter Swierstra, (Ed.) ACM, 1–12. doi:10.1145/263 3357.2633358 (cit. on pp. 24, 25)

    2014

  46. [55]

    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. In36th European Conference on Object-Oriented Programming, ECOOP 2022, Berlin, Germany, June 6-10, 2022(LIPIcs). Karim Ali and Jan Vitek, (Eds....

    2022 doi

  47. [56]

    Ningning Xie, Youyou Cong, Kazuki Ikemori, and Daan Leijen. 2022. First-class names for effect handlers.Proc. ACM Program. Lang., 6, OOPSLA2, 30–59. doi:10.1145/3563289 (cit. on p. 24)

    2022 doi

  48. [57]

    Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2023. Making a type difference: Subtraction on intersection types as generalized record operations.Proc. ACM Program. Lang., 7, POPL, 893–920. doi:10.1145/3571224 (cit. on p. 24)

    2023 doi

  49. [58]

    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 pp. 23, 24)

    2024 doi

  50. [59]

    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. 1, 3, 5–7, 10–13, 17, 18, 22–24, 30)

    2025 doi

  51. [60]

    Yichen Xu and Martin Odersky. 2023. Formalizing box inference for capture calculus. (2023). https://arxiv.org/abs/23 06.06496 arXiv: 2306.06496[cs.PL](cit. on p. 18)

    2023 arXiv

  52. [61]

    Takuma Yoshioka, Taro Sekiyama, and Atsushi Igarashi. 2024. Abstracting effect systems for algebraic effect handlers. Proc. ACM Program. Lang., 8, ICFP, 455–484. doi:10.1145/3674641 (cit. on p. 25)

    2024 doi

  53. [62]

    Yizhou Zhang and Andrew C. Myers. 2019. Abstraction-safe effect handlers via tunneling.Proc. ACM Program. Lang., 3, POPL, 5:1–5:29. doi:10.1145/3290318 (cit. on pp. 22, 25)

    2019 doi

  54. [63]

    Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers. 2016. Accepting blame for safe tunneled exceptions. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June...

    2016

  55. [2009]

    doi:10.1145/1481861.1481868 (cit

    Andrew Kennedy and Amal Ahmed, (Eds.) ACM, 39–50. doi:10.1145/1481861.1481868 (cit. on p. 19)

  56. [2021]

    InSCALA 2021: Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, Chicago, IL, USA, 17 October 2021

    Safer exceptions for Scala. InSCALA 2021: Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, Chicago, IL, USA, 17 October 2021. Julien Richard-Foy and Sébastien Doeraene, (Eds.) ACM, 1–11. doi:10.1145/3 486610.3486893 (cit. on pp. 1, 4, 5, 22, 25)

    2021

  57. [2023]

    Capturing types.ACM Trans. Program. Lang. Syst., 45, 4, 21:1–21:52. doi:10.1145/3618003 (cit. on pp. 1, 3, 12, 13, 16, 22, 23, 35)

    doi

  58. [2024]

    ACM Program

    Qualifying System F<:: Some terms and conditions may apply.Proc. ACM Program. Lang., 8, OOPSLA1, 583–612. doi:10.1145/3649832 (cit. on pp. 2, 23, 25). Classifying Capabilities (Extended Version) 27

    doi

Pith tools

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