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. Unlike previous type systems for region-based memory management, our formalism allows us to give a syntactic proof of type soundness using standard techniques. We demonstrate the expressiveness of the language by sketching a translating Tofte and Talpin's high-level type-and-effects system for region-based memory management into our language.

(postscript)