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
Type
conference paper
DOI
10.1145/3660829.3660851
Scopus ID

2-s2.0-85199115105

Author(s)
Xu, Yichen  

École Polytechnique Fédérale de Lausanne

Odersky, Martin  

École Polytechnique Fédérale de Lausanne

Editors
Soderberg, Emma
•
Church, Luke
Date Issued

2024-03-11

Publisher

Association for Computing Machinery, Inc

Published in
Programming Companion 2024 - Proceedings of the 8th International Conference on on the Art, Science, and Engineering of Programming
ISBN of the book

9798400706349

Start page

134

End page

138

Subjects

Capture Calculus

•

Mutable Variables

•

Scala

•

Type Systems

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LAMP1  
Event nameEvent acronymEvent placeEvent date
8 International Conference on on the Art, Science, and Engineering of Programming

Lund, Sweden

2024-03-11 - 2024-03-15

Available on Infoscience
January 26, 2025
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/244845
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