TY - GEN
T1 - Conflation confers concurrency
AU - Atkey, Robert
AU - Lindley, Sam
AU - Morris, J. Garrett
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84973872434&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-30936-1_2
DO - 10.1007/978-3-319-30936-1_2
M3 - Conference contribution
AN - SCOPUS:84973872434
SN - 9783319309354
T3 - Lecture Notes in Computer Science
SP - 32
EP - 55
BT - A List of Successes that can Change the World
A2 - Trinder, Phil
A2 - McBride, Conor
A2 - Lindley, Sam
A2 - Sannella, Don
PB - Springer
ER -