Managing Memory with Types (Thesis)

Abstract:

Important programming language features require specific memory-management
techniques. General recursion requires the automatic stack allocation of
local variables. Higher-order functions and object-oriented techniques
require sophisticated services, such as garbage collection, to manage
memory. When memory is a scare resource it is important for the programmer
to explicitly control memory management. Unfortunately, a programmer can
accidentally destroy important program properties and violate the integrity
of the program through memory management related errors.

By using modern type systems, we can expose low-level memory management
services to programmers and type-preserving compilers in a way that still
guarantees the integrity of the program. We can build more sophisticated
memory management services by using these low-level services in a way that
provides useful guarantees about program integrity.

I combine existing type systems with several standard type-based compilation
techniques to write strongly typed programs that include a function that
acts as a tracing garbage collector for the program. Since the garbage
collector is an explicit function, there is no need to provide a trusted
garbage collector as a runtime service to manage memory. Since the language
is strongly typed, the standard type soundness guarantee ``Well typed
programs do not go wrong'' is extended to include the collector, making the
garbage collector an untrusted piece of code. This is a desirable property
for both Java and proof-carrying code systems.

I describe the technique in detail and report performance measurements for a
prototype system as well as present the proofs of type soundness for
important subsets of our system, and describe how to use types as a
mechanism to manage memory in explicit and safe ways.