Authors
Stefan Monnier
Zhong Shao
Abstract
Standard type systems are not sufficiently expressive when applied to
low-level memory-management code. Such code often uses some form of strong
update (i.e. assignments that change the type of the affected location)
and needs to reason about the relative position of objects in memory.
We present a novel type system which, like alias types, provides
a form of strong update, but with the advantage that it does not require the
aliasing pattern to be statically described. It also provides operations
over sequential memory locations and allows covariant reference casts.
We then show how this new type system can be used to implement
a type-safe stop© garbage collector that can properly collect
cyclic data-structures. More specifically, we show how
to write a two-generations collector for a language with mutable
ref-cells.
Published
Technical Report YALEU/DCS/TR-1242, Department of
Computer Science, Yale University, October 2002.