Journal article

Title:
Capturing Types
Authors:
A. Boruch-Gruszecki, M. Odersky, E. Lee, O. Lhoták, J. Brachthäuser
Publication:
ACM Trans. Program. Lang. Syst. 45 (4)
DOI:
10.1145/3618003
Year:
2023
Link:
https://dl.acm.org/doi/10.1145/3618003

Abstract:
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC< :◻, a calculus where such captured variables are succinctly represented in types, and show it can be used to safely implement effects and effect polymorphism via scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that CC< :◻  admits simple and intuitive types for common data structures and their typical usage patterns. We demonstrate how these ideas can be used to guide the implementation of capture checking in a practical programming language.

BibTeX:
@article{boruchgruszecki_capturing_2023,
    title = {{Capturing Types}},
    author = {Boruch-Gruszecki, Aleksander and Odersky, Martin and Lee, Edward and Lhoták, Ondřej and Brachthäuser, Jonathan},
    year = {2023},
    journal = {{ACM Trans. Program. Lang. Syst.}},
    number = {4},
    doi = {10.1145/3618003},
    issn = {0164-0925},
    pages = {21:1--21:52},
    url = {https://dl.acm.org/doi/10.1145/3618003},
    volume = {45},
}