Conflation confers concurrency

Atkey, Robert and Lindley, Sam and Morris, J. Garrett (2016) Conflation confers concurrency. In: A List of Successes That Can Change the World. Lecture Notes in Computer Science, 9600 . Springer, pp. 32-55. ISBN 9783319309354

[img]
Preview
Text (Atkey-etal-LNCS2016-conflation-confers-concurrency)
Atkey_etal_LNCS2016_conflation_confers_concurrency.pdf
Accepted Author Manuscript

Download (397kB)| Preview

    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.