Last modified: Fri Jun 22 14:57:50 2001 GMT.
AbstractProof-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.
PublishedIn Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01), Salt Lake City, Utah, pages 81-91, June 2001. ©2001 ACM.
Copyright © 1996-2023 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science