SPLASH 2026
Sun 4 - Fri 9 October 2026 Oakland, California, United States
co-located with SPLASH/ISSTA 2026

Capture checking in Scala 3 enables lightweight and practical effect and resource 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.

Mon 5 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 15:00
Set-Theoretic Types and Object EvolutionOOPSLA at Junior Ballroom 1&2
Chair(s): Jonathan Aldrich Carnegie Mellon University
13:30
18m
Talk
Implementing Set-Theoretic Types
OOPSLA
Mickaël Laurent Charles University, Kim Nguyễn Université Paris-Saclay
DOI File Attached
13:48
18m
Talk
Modular Type Safety for Traits with Extensible Variants and Deep Pattern Matching
OOPSLA
Andong Fan University of Toronto, Lionel Parreaux Hong Kong University of Science and Technology, Ningning Xie University of Toronto
DOI
14:06
18m
Talk
Type-Safe Monotonic Object Evolution
OOPSLA
Alexandra Mirrlees-Black Australian National University, Haoyu Wu Australian National University, Gregor Richards University of Waterloo, Fabian Muehlboeck Australian National University
DOI Pre-print
14:24
18m
Talk
Classifying Capabilities
OOPSLA
DOI