On regions and linear types

D. Walker; K. Watkins

On regions and linear types

Research output: Contribution to conference › Paper › peer-review

Abstract

We explore how two different mechanisms for reasoning about state, linear typing and the type, region and effect discipline, complement one another in the design of a strongly typed functional programming language. The basis for our language is a simple lambda calculus containing first-class memory regions, which are explicitly passed as arguments to functions, returned as results and stored in user-defined data structures. In order to ensure appropriate memory safety properties, we draw upon the literature on linear type systems to help control access to and deallocation of regions. In fact, we use two different interpretations of linear types, one in which multiple-use values are freely copied and discarded and one in which multiple-use values are explicitly reference-counted, and show that both interpretations give rise to interesting invariants for manipulating regions. We also explore new programming paradigms that arise by mixing first-class regions and conventional linear data structures.

Original language	American English
Pages	181-192
Number of pages	12
State	Published - 2001
Externally published	Yes
Event	6th ACM SIGPLAN Internatinal Conference on Functional Programming (ICFP'01) - Florence, Italy Duration: Sep 3 2001 → Sep 5 2001

Conference

Conference	6th ACM SIGPLAN Internatinal Conference on Functional Programming (ICFP'01)
Country/Territory	Italy
City	Florence
Period	9/3/01 → 9/5/01

ASJC Scopus subject areas

Software

Cite this

@conference{1b7bd38ee3974691912b5c97f752e735,

title = "On regions and linear types",

abstract = "We explore how two different mechanisms for reasoning about state, linear typing and the type, region and effect discipline, complement one another in the design of a strongly typed functional programming language. The basis for our language is a simple lambda calculus containing first-class memory regions, which are explicitly passed as arguments to functions, returned as results and stored in user-defined data structures. In order to ensure appropriate memory safety properties, we draw upon the literature on linear type systems to help control access to and deallocation of regions. In fact, we use two different interpretations of linear types, one in which multiple-use values are freely copied and discarded and one in which multiple-use values are explicitly reference-counted, and show that both interpretations give rise to interesting invariants for manipulating regions. We also explore new programming paradigms that arise by mixing first-class regions and conventional linear data structures.",

author = "D. Walker and K. Watkins",

year = "2001",

language = "American English",

pages = "181--192",

note = "6th ACM SIGPLAN Internatinal Conference on Functional Programming (ICFP'01) ; Conference date: 03-09-2001 Through 05-09-2001",

}

TY - CONF

T1 - On regions and linear types

AU - Walker, D.

AU - Watkins, K.

PY - 2001

Y1 - 2001

N2 - We explore how two different mechanisms for reasoning about state, linear typing and the type, region and effect discipline, complement one another in the design of a strongly typed functional programming language. The basis for our language is a simple lambda calculus containing first-class memory regions, which are explicitly passed as arguments to functions, returned as results and stored in user-defined data structures. In order to ensure appropriate memory safety properties, we draw upon the literature on linear type systems to help control access to and deallocation of regions. In fact, we use two different interpretations of linear types, one in which multiple-use values are freely copied and discarded and one in which multiple-use values are explicitly reference-counted, and show that both interpretations give rise to interesting invariants for manipulating regions. We also explore new programming paradigms that arise by mixing first-class regions and conventional linear data structures.

AB - We explore how two different mechanisms for reasoning about state, linear typing and the type, region and effect discipline, complement one another in the design of a strongly typed functional programming language. The basis for our language is a simple lambda calculus containing first-class memory regions, which are explicitly passed as arguments to functions, returned as results and stored in user-defined data structures. In order to ensure appropriate memory safety properties, we draw upon the literature on linear type systems to help control access to and deallocation of regions. In fact, we use two different interpretations of linear types, one in which multiple-use values are freely copied and discarded and one in which multiple-use values are explicitly reference-counted, and show that both interpretations give rise to interesting invariants for manipulating regions. We also explore new programming paradigms that arise by mixing first-class regions and conventional linear data structures.

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

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

M3 - Paper

SP - 181

EP - 192

T2 - 6th ACM SIGPLAN Internatinal Conference on Functional Programming (ICFP'01)

Y2 - 3 September 2001 through 5 September 2001

ER -

On regions and linear types

Abstract

Conference

ASJC Scopus subject areas

Other files and links

Fingerprint

Cite this