Alias types

Frederick Smith; David Walker; Greg Morrisett

doi:10.1007/3-540-46425-5_24

Alias types

Frederick Smith, David Walker, Greg Morrisett

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

126 Scopus citations

Abstract

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.

Original language	English (US)
Title of host publication	Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings
Editors	Gert Smolka
Publisher	Springer Verlag
Pages	366-381
Number of pages	16
ISBN (Print)	3540672621, 9783540672623
DOIs	https://doi.org/10.1007/3-540-46425-5_24
State	Published - 2000
Externally published	Yes
Event	9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 - Berlin, Germany Duration: Mar 25 2000 → Apr 2 2000

Publication series

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

Other

Other	9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000
Country/Territory	Germany
City	Berlin
Period	3/25/00 → 4/2/00

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-46425-5_24

Cite this

Smith, F., Walker, D., & Morrisett, G. (2000). Alias types. In G. Smolka (Ed.), Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings (pp. 366-381). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1782). Springer Verlag. https://doi.org/10.1007/3-540-46425-5_24

Smith, Frederick ; Walker, David ; Morrisett, Greg. / Alias types. Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. editor / Gert Smolka. Springer Verlag, 2000. pp. 366-381 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{b8ace3929f864b59a47cae54493048af,

title = "Alias types",

abstract = "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.",

author = "Frederick Smith and David Walker and Greg Morrisett",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 ; Conference date: 25-03-2000 Through 02-04-2000",

year = "2000",

doi = "10.1007/3-540-46425-5_24",

language = "English (US)",

isbn = "3540672621",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "366--381",

editor = "Gert Smolka",

booktitle = "Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings",

address = "Germany",

}

Smith, F, Walker, D & Morrisett, G 2000, Alias types. in G Smolka (ed.), Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1782, Springer Verlag, pp. 366-381, 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, 3/25/00. https://doi.org/10.1007/3-540-46425-5_24

Alias types. / Smith, Frederick; Walker, David; Morrisett, Greg.
Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. ed. / Gert Smolka. Springer Verlag, 2000. p. 366-381 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1782).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Alias types

AU - Smith, Frederick

AU - Walker, David

AU - Morrisett, Greg

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2000.

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84947255140&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947255140&partnerID=8YFLogxK

U2 - 10.1007/3-540-46425-5_24

DO - 10.1007/3-540-46425-5_24

M3 - Conference contribution

AN - SCOPUS:84947255140

SN - 3540672621

SN - 9783540672623

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 366

EP - 381

BT - Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings

A2 - Smolka, Gert

PB - Springer Verlag

T2 - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000

Y2 - 25 March 2000 through 2 April 2000

ER -

Smith F, Walker D, Morrisett G. Alias types. In Smolka G, editor, Programming Languages and Systems - 9th European Symposium on Programming, ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Proceedings. Springer Verlag. 2000. p. 366-381. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-46425-5_24

Alias types

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this