Typed memory management via static capabilities

Region-based memory management is an alternative to standard tracing garbag e collection that makes operations such as memory deallocation explicit but verifiably safe. In this article, we present a new compiler intermediate l anguage, called the Capability Language (CL), that supports region-based me mory management and enjoys a provably safe type system. Unlike previous reg ion-based type systems, region lifetimes need not be lexically scoped, and yet the language may be checked for safety without complex analyses. Theref ore, our type system may be deployed in settings such as extensible operati ng systems where both the performance and safety of untrusted code is impor tant. The central novelty of the language is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure capabilities are relinquished properl y, the type system tracks aliasing information using a form of bounded quan tification. Moreover, unlike previous work on region-based type systems, th e proof of soundness of our type system is relatively simple, employing onl y standard syntactic techniques. In order to show how our language may be u sed in practice, we show how to translate a variant of Tofte and Talpin's h igh-level type-and-effects system for region-based memory management into o ur language. When combined with known region inference algorithms, this tra nslation provides a way to compile source-level languages to CL.