A Formal Foundation of Reach CapabilitiesVIMPL
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 MarDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:00 - 12:00 | |||
10:00 60mKeynote | Lightweight Affine Types for Safe Concurrency in ScalaVIMPL VIMPL Link to publication | ||
11:00 30mPaper | A Formal Foundation of Reach CapabilitiesVIMPL VIMPL | ||
11:30 30mTalk | Tinyrossa: a compiler framework for vertical, verified construction of Smalltalk VMs MoreVMs |