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 language | English |
---|---|
Article number | 33 |
Journal | Leibniz International Proceedings in Informatics (LIPIcs) |
Volume | 59 |
Pages (from-to) | 1-15 |
Number of pages | 15 |
ISSN | 1868-8969 |
DOIs | |
Publication status | Published - 2016 |
Keywords
- Classical Processes
- Multiparty Session Types
- Linear Logic
- Calculus of Processes
- Coherence Proofs