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

Abstract / Description of output

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)
Place of PublicationQuébec City, Canada
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages15
ISBN (Print)978-3-95977-017-0
Publication statusPublished - 24 Aug 2016
Event27th International Conference on Concurrency Theory - Québec City, Canada
Duration: 23 Aug 201626 Aug 2016

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISSN (Print)1868-8969


Conference27th International Conference on Concurrency Theory
Abbreviated titleCONCUR 2016
CityQuébec City
Internet address


Dive into the research topics of 'Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types'. Together they form a unique fingerprint.

Cite this