Alias Types for 

Recursive Data Structures

(Extended Version)


Linear type systems permit programmers to deallocate or explicitly
recycle memory, but they are severely restricted by the fact that they
admit no aliasing. This paper describes a pseudo-linear type system
that allows a degree of aliasing and memory reuse as well as the
ability to define complex recursive data structures. Our type system
can encode conventional linear data structures such as linear lists
and trees as well as more sophisticated data structures including
cyclic and doubly-linked lists and trees. In the latter cases, our
type system is expressive enough to represent pointer aliasing and yet
safely permit destructive operations such as object deallocation. We
demonstrate the flexibility of our type system by encoding two common
compiler optimizations: destination-passing style and
Deutsch-Schorr-Waite or "link-reversal'' traversal algorithms.

(pdf, ps.gz)