Coherence generalises duality: A logical explanation of multiparty session types

Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, Philip Wadler

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

41 Citations (Scopus)


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.

Original languageEnglish
Title of host publication27th International Conference on Concurrency Theory (CONCUR 2016)
EditorsJosee Desharnais, Radha Jagadeesan
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
ISBN (Electronic)9783959770170
Publication statusPublished - 24 Aug 2016
Event27th International Conference on Concurrency Theory 2016 - Quebec City, Canada
Duration: 23 Aug 201626 Aug 2016

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
ISSN (Print)1868-8969


Conference27th International Conference on Concurrency Theory 2016
Abbreviated titleCONCUR 2016
CityQuebec City


  • Linear logic
  • Multiparty session types
  • Propositions as types

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Coherence generalises duality: A logical explanation of multiparty session types'. Together they form a unique fingerprint.

Cite this