System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)
Yichen Xu, Oliver Bračevac, Cao Nguyen Pham, Yaoyu Zhao, Martin Odersky
cs.PL
Jul 10, 2026 · v1
TL;DR
The core calculus CoreCapybara's semantic soundness (type, memory safety, immutability) is mechanized in Lean 4.
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.
Problem
Substructural type systems give strong static alias control, but retrofitting such guarantees into languages like Scala that rely on unrestricted aliasing and pervasive sharing is difficult. The goal is to add selective alias-control guarantees without imposing global invariants.
Approach
System Capybara adds a selective alias-control layer to Scala's capture checking, tracking separation, consumption, freshness, and read-only access for capabilities. A type-preserving translation maps the surface calculus to CoreCapybara, a core calculus extending System Capless with modal types, existential capture types, and reader values. A logical relation model of CoreCapybara is developed and its semantic soundness is mechanized in Lean 4.
Results
Semantic soundness of CoreCapybara yields type safety, memory safety (no use-after-free or double-free), immutability of read-only computations, and, via confluence, data-race freedom for well-typed programs. A separation checker was implemented in Scala 3.