Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types

Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann 0001, Philip Wadler [2016].
In proceedings of CONCUR 2016, pp. 33:1-33:15.

Abstract

Wadler introduced Classical Processes (CP), a calculus based on a propositions-as-types correspondence between propositions of classical linear logic and session types. Carbone et al. introduced Multiparty Classical Processes, a calculus that generalises CP to multiparty session types, by replacing the duality of classical linear logic (relating two types) with a more general notion of coherence (relating an arbitrary number of types). This paper introduces variants of CP and MCP, plus a new intermediate calculus of Globally-governed Classical Processes (GCP). We show a tight relation between these three calculi, giving semantics-preserving translations from GCP to CP and from MCP to GCP. The translation from GCP to CP interprets a coherence proof as an arbiter process that mediates communications in a session, while MCP adds annotations that permit processes to communicate directly without centralised control.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/concur/CarboneLMSW16,
  author       = {Marco Carbone and
                  Sam Lindley and
                  Fabrizio Montesi and
                  Carsten Sch{\"{u}}rmann and
                  Philip Wadler},
  editor       = {Jos{\'{e}}e Desharnais and
                  Radha Jagadeesan},
  title        = {Coherence Generalises Duality: {A} Logical Explanation of Multiparty
                  Session Types},
  booktitle    = {27th International Conference on Concurrency Theory, {CONCUR} 2016,
                  August 23-26, 2016, Qu{\'{e}}bec City, Canada},
  series       = {LIPIcs},
  volume       = {59},
  pages        = {33:1--33:15},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2016},
  url          = {https://doi.org/10.4230/LIPIcs.CONCUR.2016.33},
  doi          = {10.4230/LIPICS.CONCUR.2016.33},
  timestamp    = {Wed, 10 Jan 2024 22:27:40 +0100},
  biburl       = {https://dblp.org/rec/conf/concur/CarboneLMSW16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):

Some data from DBLP and Crossref.