Regions, part 2: The Capability Calculus
Abstract
|
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.
|
Slides
|
