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 proceedingArticle in proceedingsResearchpeer-review

67 Downloads (Pure)

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. © Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler; licensed under Creative Commons License CC-BY.
Original languageEnglish
Title of host publicationProceedings of the 27th International Conference on Concurrency Theory
EditorsJosée Desharnais, Radha Jagadeesan
PublisherSchloss Dagstuhl-Leibniz-Zentrum fuer Informatik
Publication date2016
Pages1–15
Article number33
ISBN (Electronic)978-3-95977-017-0
DOIs
Publication statusPublished - 2016
Event27th International Conference on Concurrency Theory - Québec City, Canada
Duration: 23. Aug 201626. Aug 2016
Conference number: 27

Conference

Conference27th International Conference on Concurrency Theory
Number27
Country/TerritoryCanada
CityQuébec City
Period23/08/201626/08/2016
SeriesLeibniz International Proceedings in Informatics
Volume59
ISSN1868-8969

Keywords

  • Linear logic
  • Multiparty session types
  • Propositions as types

Cite this