Type-Preserving Garbage Collectors (Extended Version)

Abstract:

By combining existing type systems with standard type-based compilation
techniques, we describe how 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, we do not need to provide a
trusted garbage collector as a runtime service to manage memory.

Since our language is strongly typed, the standard type soundness
guarantee ``Well typed programs do not go wrong'' is extended to
include the collector. Our type safety guarantee is non-trivial since
not only does it guarantee the type safety of the garbage collector,
but it guarantees that the collector preservers the type safety of the
program being garbage collected. We describe the technique in detail
and report performance measurements for a few microbenchmark. We also
include a formal semantics for a novel region calculus that supports
early deallocation, and prove the type soundness of the system.