Skip to main content
PRL Project

Regions, part 2: The Capability Calculus

by David Walker


Last week I motivated region-based memory management, described an implementation in the ML kit with region, and gave a high-level overview of the basic principles involved. This week I will investigate region-based memory management in more detail with emphasis on a type system that ensures safety. However, instead of explaining Tofte and Talpin's (TT) region-based type system, I will discuss my own work (with Karl Crary and Greg Morrisett) on the "Calculus of Capabilities." I'll point out some of the limitations of TT that prevent us from using this language as a type-safe and flexible low-level language. Then I'll show how to address these problems by replacing the effects that appear in a region-based type system with a notion of a "static capability." These capabilities mediate access to memory in a safe but flexible way. Along the way, I will explain some of the connections between these static capabilities and linear logic. Time permitting, I will mention some further applications of this notion of capability and discuss future directions for research.


The talk was based on the paper "Typed Memory Management in a Calculus of Capabilities."

David Walker's research on safe static memory management