Conflation confers concurrency

Robert Atkey, Sam Lindley, J. Garrett Morris

Research output: Chapter in Book/Report/Conference proceedingChapter

  • 3 Citations

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.
LanguageEnglish
Title of host publicationA List of Successes That Can Change the World
Subtitle of host publicationEssays Dedicated to Philip Wadler on the Occasion of His 60th Birthday
EditorsSam Lindley, Conor McBride, Phil Trinder, Don Sannella
PublisherSpringer
Pages32-55
Number of pages24
Volume9600
ISBN (Print)9783319309354
DOIs
StatePublished - 28 Apr 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9600

Fingerprint

Network protocols
Communication

Keywords

  • proof rules
  • cut reduction
  • linear logic
  • process calculi

Cite this

Atkey, R., Lindley, S., & Morris, J. G. (2016). Conflation confers concurrency. In S. Lindley, C. McBride, P. Trinder, & D. Sannella (Eds.), A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Vol. 9600, pp. 32-55). (Lecture Notes in Computer Science; Vol. 9600). Springer. DOI: 10.1007/978-3-319-30936-1_2
Atkey, Robert ; Lindley, Sam ; Morris, J. Garrett. / Conflation confers concurrency. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. editor / Sam Lindley ; Conor McBride ; Phil Trinder ; Don Sannella. Vol. 9600 Springer, 2016. pp. 32-55 (Lecture Notes in Computer Science).
@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 = "4",
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",

}

Atkey, R, Lindley, S & Morris, JG 2016, Conflation confers concurrency. in S Lindley, C McBride, P Trinder & D Sannella (eds), A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. vol. 9600, Lecture Notes in Computer Science, vol. 9600, Springer, pp. 32-55. DOI: 10.1007/978-3-319-30936-1_2

Conflation confers concurrency. / Atkey, Robert; Lindley, Sam; Morris, J. Garrett.

A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. ed. / Sam Lindley; Conor McBride; Phil Trinder; Don Sannella. Vol. 9600 Springer, 2016. p. 32-55 (Lecture Notes in Computer Science; Vol. 9600).

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - Conflation confers concurrency

AU - Atkey,Robert

AU - Lindley,Sam

AU - Morris,J. Garrett

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-30936-1_2

PY - 2016/4/28

Y1 - 2016/4/28

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.

KW - proof rules

KW - cut reduction

KW - linear logic

KW - process calculi

UR - http://bentnib.org/conflate.html

U2 - 10.1007/978-3-319-30936-1_2

DO - 10.1007/978-3-319-30936-1_2

M3 - Chapter

SN - 9783319309354

VL - 9600

T3 - Lecture Notes in Computer Science

SP - 32

EP - 55

BT - A List of Successes That Can Change the World

PB - Springer

ER -

Atkey R, Lindley S, Morris JG. Conflation confers concurrency. In Lindley S, McBride C, Trinder P, Sannella D, editors, A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Vol. 9600. Springer. 2016. p. 32-55. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-30936-1_2