Typed memory management in a calculus of capabilities

An increasing number of systems rely on programming lan-guage technology to ensure safety and security of low-level code. Unfortunately, these systems typically rely on a com-plex, trusted garbage collector. Region-based type systems provide an alternative to garbage collection by making mem-ory management explicit but veriably safe. However, it has not been clear how to use regions in low-level, type-safe code. We present a compiler intermediate language, called the Capability Calculus, that supports region-based memory management, enjoys a provably safe type system, and is straightforward to compile to a typed assembly language. Source languages may be compiled to our language using known region inference algorithms. Furthermore, region life-times need not be lexically scoped in our language, yet the language may be checked for safety without complex anal-yses. Finally, our soundness proof is relatively simple, em-ploying only standard techniques. The central novelty is the use of static capabilities to specify the permissibility of various operations, such as memory access and deallocation. In order to ensure ca-pabilities are relinquished properly, the type system tracks aliasing information using a form of bounded quantication.