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.

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.
Additional notes
Cite (BibTeX)
Click to expand
  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          = {},
  doi          = {10.4230/LIPICS.CONCUR.2016.33},
  timestamp    = {Wed, 10 Jan 2024 22:27:40 +0100},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}

A PDF is available (possibly a preprint):

Download PDF