‹Programming› 2024
Mon 11 - Fri 15 March 2024 Lund, Sweden
Tue 12 Mar 2024 11:00 - 11:30 at M:G - Safety and Correctness Chair(s): Dimi Racordon

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 better 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<:□ that formalises reach capabilities. This abstract describes the system and prospects the formal properties that should be established for it.

Tue 12 Mar

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change