Conflation confers concurrency

Robert Atkey*, Sam Lindley, J. Garrett Morris

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

25 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationA List of Successes that can Change the World
EditorsPhil Trinder, Conor McBride, Sam Lindley, Don Sannella
PublisherSpringer
Pages32-55
Number of pages24
ISBN (Electronic)9783319309361
ISBN (Print)9783319309354
DOIs
Publication statusPublished - 2016

Publication series

NameLecture Notes in Computer Science
Volume9600
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Conflation confers concurrency'. Together they form a unique fingerprint.

Cite this