Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types

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

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review

Abstrakt

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.
OriginalsprogEngelsk
Artikelnummer33
TidsskriftLeibniz International Proceedings in Informatics (LIPIcs)
Vol/bind59
Sider (fra-til)1-15
Antal sider15
ISSN1868-8969
DOI
StatusUdgivet - 2016

Fingeraftryk

Dyk ned i forskningsemnerne om 'Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types'. Sammen danner de et unikt fingeraftryk.

Citationsformater