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

15 Citations (Scopus)

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.

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
DOIs
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)
Volume59
ISSN (Print)1868-8969

Conference

Conference27th International Conference on Concurrency Theory 2016
Abbreviated titleCONCUR 2016
CountryCanada
CityQuebec City
Period23/08/1626/08/16

Keywords

  • Linear logic
  • Multiparty session types
  • Propositions as types

ASJC Scopus subject areas

  • Software

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

  • Cite this

    Carbone, M., Lindley, S., Montesi, F., Schürmann, C., & Wadler, P. (2016). Coherence generalises duality: A logical explanation of multiparty session types. In J. Desharnais, & R. Jagadeesan (Eds.), 27th International Conference on Concurrency Theory (CONCUR 2016) [33] (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 59). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2016.33