Book chapter
Conflation Confers Concurrency
A List of Successes That Can Change the World, pp.32-55
Lecture Notes in Computer Science, v. 9600, Springer International Publishing
03/25/2016
DOI: 10.1007/978-3-319-30936-1_2
Abstract
Session types provide a static guarantee that concurrent programs respect communication protocols. Recent work has explored a correspondence between proof rules and cut reduction in linear logic and typing and evaluation of process calculi. This paper considers two approaches to extend logically-founded process calculi. First, we consider extensions of the process calculus to more closely resemble π-calculus. Second, inspired by denotational models of process calculi, we consider conflating dual types. Most interestingly, we observe that these approaches coincide: conflating the multiplicatives (⊗ and) allows processes to share multiple channels; conflating the additives (⊕ and &) provides nondeterminism; and conflating the exponentials (! and ?) yields access points, a rendezvous mechanism for initiating session typed communication. Access points are particularly expressive: for example, they are sufficient to encode concurrent state and general recursion.
Details
- Title: Subtitle
- Conflation Confers Concurrency
- Creators
- Robert Atkey - University of StrathclydeSam Lindley - University of EdinburghJ. Garrett Morris - University of Edinburgh
- Resource Type
- Book chapter
- Publication Details
- A List of Successes That Can Change the World, pp.32-55
- Series
- Lecture Notes in Computer Science; v. 9600
- DOI
- 10.1007/978-3-319-30936-1_2
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Publisher
- Springer International Publishing; Cham
- Language
- English
- Date published
- 03/25/2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984410844202771
Metrics
18 Record Views