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 language | English |
---|---|
Title of host publication | Proceedings of the 27th International Conference on Concurrency Theory |
Editors | Josée Desharnais, Radha Jagadeesan |
Publisher | Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik |
Publication date | 2016 |
Pages | 1–15 |
Article number | 33 |
ISBN (Electronic) | 978-3-95977-017-0 |
DOIs | |
Publication status | Published - 2016 |
Event | 27th International Conference on Concurrency Theory - Québec City, Canada Duration: 23. Aug 2016 → 26. Aug 2016 Conference number: 27 |
Conference
Conference | 27th International Conference on Concurrency Theory |
---|---|
Number | 27 |
Country/Territory | Canada |
City | Québec City |
Period | 23/08/2016 → 26/08/2016 |
Series | Leibniz International Proceedings in Informatics |
---|---|
Volume | 59 |
ISSN | 1868-8969 |
Keywords
- Linear logic
- Multiparty session types
- Propositions as types