A Formal Foundation of Reach Capabilities

Though being seemingly orthogonal, the scoping restrictions enforced by capture checking and mutable variables give rise to surprising challenges when they interact. To obtain a system that is both sound and expressive, the Scala capture checker introduced reach capabilities. Although the empirical evaluation shows that the system is expressive enough to capture check the Scala standard library, its soundness remains unresolved: in fact, it has known soundness issues. Unfortunately, the core calculus models neither reach capabilities nor mutable variables, so a formal foundation for them is lacking. To bridge the gap between the implementation and the theory and to gain a better understanding of the reach capabilities approach, we present System CC◦, a mild extension to System CC