Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types

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

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

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
Article number33
JournalLeibniz International Proceedings in Informatics (LIPIcs)
Volume59
Pages (from-to)1-15
Number of pages15
ISSN1868-8969
DOIs
Publication statusPublished - 2016

Keywords

  • Classical Processes
  • Multiparty Session Types
  • Linear Logic
  • Calculus of Processes
  • Coherence Proofs

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