Published papers, technical reports, and talks online.


Stefan Monnier
Bratin Saha
Zhong Shao


Proof-carrying code and typed assembly languages aim to minimize the trusted computing base by directly certifying the actual machine code. Unfortunately, these systems cannot get rid of the dependency on a trusted garbage collector. 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 techniques for writing type-safe stop-and-copy garbage collectors. We show how to use 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-program analysis), our new framework directly supports higher-order funtions and is compatible with separate compilation; our collectors are written in provably type-safe languages with rigorous semantics and fully formalized soundness proofs.


In Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01), Salt Lake City, Utah, pages 81-91, June 2001. ©2001 ACM. Technical Report YALEU/DCS/TR-1205, Department of Computer Science, Yale University, Nov 2000.