Sciweavers

Share
POPL
1999
ACM

Typed Memory Management in a Calculus of Capabilities

9 years 1 months ago
Typed Memory Management in a Calculus of Capabilities
An increasing number of systems rely on programming language technology to ensure safety and security of low-level code. Unfortunately, these systems typically rely on a complex, trusted garbage collector. Region-based type systems provide an alternative to garbage collection by making memory management explicit but verifiably 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 lifetimes need not be lexically scoped in our language, yet the language may be checked for safety without complex analyses. Finally, our soundness proof is relatively simple, employing only standard techniques. The central novelty is the use of stat...
Karl Crary, David Walker, J. Gregory Morrisett
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where POPL
Authors Karl Crary, David Walker, J. Gregory Morrisett
Comments (0)
books