Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. A Formal Foundation of Reach Capabilities
 
conference paper

A Formal Foundation of Reach Capabilities

Xu, Yichen  
•
Odersky, Martin  
Soderberg, Emma
•
Church, Luke
March 11, 2024
Programming Companion 2024 - Proceedings of the 8th International Conference on on the Art, Science, and Engineering of Programming
8 International Conference on on the Art, Science, and Engineering of Programming

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

  • Details
  • Metrics
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés