Alias Types for Recursive Data Structures

David Walker and Greg Morrisett

To appear at ACM SIGPLAN Workshop on Types in Compilation (TIC00), Montreal, Canada, 21 September 2000


Linear type systems permit programmers to deallocate or explicitly recycle memory, but 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.

Server START Conference Manager
Update Time 27 Jul 2000 at 15:10:31
Start Conference Manager
Conference Systems