On regions and linear types

D. Walker, K. Watkins

Research output: Contribution to conferencePaper

30 Scopus citations

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 languageEnglish (US)
Pages181-192
Number of pages12
StatePublished - 2001
Externally publishedYes
Event6th ACM SIGPLAN Internatinal Conference on Functional Programming (ICFP'01) - Florence, Italy
Duration: Sep 3 2001Sep 5 2001

Other

Other6th ACM SIGPLAN Internatinal Conference on Functional Programming (ICFP'01)
CountryItaly
CityFlorence
Period9/3/019/5/01

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint Dive into the research topics of 'On regions and linear types'. Together they form a unique fingerprint.

  • Cite this

    Walker, D., & Watkins, K. (2001). On regions and linear types. 181-192. Paper presented at 6th ACM SIGPLAN Internatinal Conference on Functional Programming (ICFP'01), Florence, Italy.