ITU
ITU

Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types

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

View graph of relations

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

Downloads

No data available

ID: 81297224