System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)
2026-07-10 • Programming Languages
Programming Languages
AI summaryⓘ
The authors explore how to add strict control over shared access and aliasing, common in newer programming models, into Scala, a widely-used language that normally allows lots of sharing. They build on Scala’s existing capture checking system and introduce System Capybara, which lets programmers selectively enforce strong rules about resource use without changing all code. Their system tracks how different references to capabilities behave, ensuring safety properties like no data races or memory errors. They prove their core system is sound using formal verification and have implemented a checker in Scala 3 to help developers write safer concurrent code.
substructural type systemsaliasingcapture checkingcapabilitiesSystem Capybaraseparation logicformal verificationtype safetymemory safetyconcurrency
Authors
Yichen Xu, Oliver Bračevac, Cao Nguyen Pham, Yaoyu Zhao, Martin Odersky
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.