Principled scavenging

Proof-carrying code and typed assembly Languages aim to minimize the truste d computing base by directly certifying the actual machine code. Unfortunat ely, these systems cannot get rid of the dependency on a trusted garbage co llector. Indeed, constructing a provably type-safe garbage collector is one of the major open problems in the area of certifying compilation. Building on an idea by Wang and Appel, we present a series of new technique s for writing type-safe stop-and-copy garbage collectors. We show how to us e intensional type analysis to capture the contract between the mutator and the collector and how the same method can be applied to support Forwarding pointers and generations. Unlike Wang and Appel (which requires whole-prog ram analysis), our new framework directly supports higher-order funtions an d is compatible with separate compilation; our collectors are written in pr ovably type-safe languages with rigorous semantics and fully formalized sou ndness proofs.