Typed memory management

Programming languages with sound static type systems have significant software engineering advantages over unsafe programming languages. Types can enforce a wide variety of program invariants at compile time, making it possible to catch programmer errors early in the software development cycle. Types can also improve programming language implementations by helping to guide program transformations and optimizations. In typed intermediate languages, such as the Java Virtual Machine Language, types certify crucial safety properties needed to implement secure and reliable software systems.; One area where traditional type systems provide little help to programmers is in the specification and enforcement of memory management invariants. In this thesis, I address this problem by developing new type systems with sophisticated mechanisms for checking programs that perform their own memory management. The central goal is to make it possible for programs to control memory resources, as in unsafe languages, and yet retain the software engineering benefits of strong type systems.; The central technical novelty of these type systems is the presence of a static capability that can control access to memory resources. Capabilities are instantiated in two ways in this thesis. First, they are instantiated with specifications of individual memory blocks. These capabilities make it possible to allocate, initialize, use and recycle data structures. They also provide a mechanism for controlling and reasoning about pointer aliasing. Second, capabilities are instantiated with vast memory regions (address spaces). This second alternative provides coarser-grained memory management as regions may contain many objects and all such objects are deallocated simultaneously when a region is freed.; For each of the resulting capability-based type systems I prove two theorems to quantify their memory management properties. First, I show that the type systems are sound: Well-typed programs never dereference dangling pointers or commit other memory faults at run time. Second, I prove a garbage collection theorem that specifies how effectively well-typed programs recycle memory.