KnowledgeBase » 
SEMINAR
» ID = 523
Regions, part 2: The Capability Calculus
by David Walker
1999-2000
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.
The talk was based on the paper "Typed Memory Management in a Calculus of Capabilities."