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.