Uniqueness Typing for Resource Management in Message-Passing Concurrency

Edsko de Vries
Adrian Francalanza
Matthew Hennessy

We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness typing and affine typing to reject these ill-behaved programs.

In Mário Florido and Ian Mackie: Proceedings First International Workshop on Linearity (LINEARITY 2009), Coimbra, Portugal, 12th September 2009, Electronic Proceedings in Theoretical Computer Science 22, pp. 26–37.
Published: 30th March 2010.

ArXived at: https://dx.doi.org/10.4204/EPTCS.22.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org