Projects per year
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.
|Title of host publication||27th International Conference on Concurrency Theory (CONCUR 2016)|
|Place of Publication||Québec City, Canada|
|Publisher||Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany|
|Number of pages||15|
|Publication status||Published - 24 Aug 2016|
|Event||27th International Conference on Concurrency Theory - Québec City, Canada|
Duration: 23 Aug 2016 → 26 Aug 2016
|Name||Leibniz International Proceedings in Informatics (LIPIcs)|
|Publisher||Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik|
|Conference||27th International Conference on Concurrency Theory|
|Abbreviated title||CONCUR 2016|
|Period||23/08/16 → 26/08/16|
FingerprintDive into the research topics of 'Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types'. Together they form a unique fingerprint.
- 1 Finished