Capture Tracking

Capture Tracking is an approach to tracking the capture of capabilities in types, which has been the subject of a long collaboration with Martin Odersky, Jonathan Brachthäuser, Ondřej Lhoták, and Edward Lee, and to which a number of other people have contributed.

The foundational formal system for the approach is CC<:◻, published in TOPLAS. Its algorithmic aspects are discussed in a technical report.

Martin Odersky’s Caprese project is focused on investigating these formal foundations further and developing their applications. The particular questions include (1) How to solve the “what color is your function” problem when mixing synchronous and asynchronous programming? (2) How to express effect polymorphism without creating boilerplate? (3) How to combine manual and automatic memory management? (4) How to express high-level concurrency and parallelism, safely? (5) How to migrate large existing code bases to the new system? Find out in the slide deck here.

CC<:◻ is neither the first nor the last formalism for Capture Tracking. I discuss the developments that led to CC<:◻ in my dissertation on the “Formal Foundations of Capture Tracking”.

Capture Tracking is particularly focused on usability and ergonomics, so naturally there is an implementation, developed first and foremost by Martin Odersky. You can find out more on this page.

Work progresses on developing CC<:◻ further. A formal system which enriches it with safe concurrency (by tracking separation of capabilities) was conditionally accepted for OOPSLA 2024. Find the preprint here.

There is also ongoing work on using the Capture Tracking implementation to develop a base library for async computation in direct style. A “strawman” version of this library is available in a Github repository here.