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.
This paper is part of a broader project. Find out more!
| paper.pdf (final-paper.pdf) | 984KiB |
Thu 18 JanDisplayed time zone: London change
10:50 - 12:10 | |||
10:50 20mTalk | Quotient Haskell: Lightweight Quotient Types for All POPL | ||
11:10 20mTalk | Focusing on Refinement Typing (TOPLAS)Remote POPL Dimitrios Economou Queen's University, Canada, Neel Krishnaswami University of Cambridge, Jana Dunfield Queen's University, Kingston, Ontario Link to publication | ||
11:30 20mTalk | Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsRemote POPL Guannan Wei Purdue University, Oliver Bračevac Galois, Inc., Songlin Jia Purdue University, USA, Yuyan Bao Augusta University, Tiark Rompf Purdue University | ||
11:50 20mTalk | Capturing Types (TOPLAS) POPL Aleksander Boruch-Gruszecki EPFL, Martin Odersky EPFL, Edward Lee University of Waterloo, Ondřej Lhoták University of Waterloo, Jonathan Immanuel Brachthäuser University of Tübingen DOI File Attached | ||