Linear type systems allow destructive operations such as object
deallocation and imperative updates of functional data structures.
These operations and others, such as the ability to reuse memory at
different types, are essential in low-level typed languages. However,
traditional linear type systems are too restrictive for use in
low-level code where it is necessary to exploit pointer aliasing. We
present a new typed language that allows functions to specify the
shape of the store that they expect and to track the flow of pointers
through a computation. Our type system is expressive enough to
represent pointer aliasing and yet safely permit destructive operations.