Typed Memory Management in a Calculus of Capabilities

Abstract

Region-based memory management is an alternative to standard 
tracing garbage collection that makes potentially dangerous 
operations such as memory deallocation explicit but verifiably 
safe. In this article, we present a new compiler intermediate 
language, called the Capability Calculus, that supports region-based 
memory management and enjoys a provably safe type system. Unlike 
previous region-based type systems, region lifetimes need not be 
lexically scoped and yet the language may be checked for safety 
without complex analyses.

The central novelty of the language is the use of static capabilities to
specify the permissibility of memory management operations. In order to
ensure capabilities are relinquished properly, the type system tracks
aliasing information using bounded quantification. We demonstrate the 
expressiveness of the language by translating Tofte and Talpin's high-level 
type-and-effects system for region-based memory management into our language.

(dvi, pdf, ps.gz)