@inbook{6e8a966138b849a49dcc2db0416698cb,
title = "Conflation confers concurrency",
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.",
keywords = "proof rules, cut reduction, linear logic, process calculi",
author = "Robert Atkey and Sam Lindley and Morris, {J. Garrett}",
note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-30936-1_2",
year = "2016",
month = apr,
day = "28",
doi = "10.1007/978-3-319-30936-1_2",
language = "English",
isbn = "9783319309354",
volume = "9600",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "32--55",
editor = "Sam Lindley and Conor McBride and Phil Trinder and Don Sannella",
booktitle = "A List of Successes That Can Change the World",
}