Alias types for recursive data structures

David Walker, Greg Morrisett

Research output: Chapter in Book/Report/Conference proceedingConference contribution

78 Scopus citations

Abstract

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 space-conscious algorithms: Destination-passing style and Deutsch-Schorr-Waite or “link-reversal” traversal algorithms.

Original languageEnglish (US)
Title of host publicationTypes in Compilation - Third InternationalWorkshop, TIC 2000 Montreal, Canada, September 21, 2000 Revised Selected Papers
EditorsRobert Harper
PublisherSpringer Verlag
Pages177-206
Number of pages30
ISBN (Print)3540421963
DOIs
StatePublished - 2001
Externally publishedYes
Event3rd International Workshop on Types in Compilation, TIC 2000 - Montreal, Canada
Duration: Sep 21 2000Sep 21 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2071
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other3rd International Workshop on Types in Compilation, TIC 2000
Country/TerritoryCanada
CityMontreal
Period9/21/009/21/00

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Alias types for recursive data structures'. Together they form a unique fingerprint.

Cite this