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.