TY - GEN
T1 - Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types
AU - Carbone, Marco
AU - Lindley, Sam
AU - Montesi, Fabrizio
AU - Schürmann, Carsten
AU - Wadler, Philip
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
U2 - 10.4230/LIPIcs.CONCUR.2016.33
DO - 10.4230/LIPIcs.CONCUR.2016.33
M3 - Conference article
VL - 59
SP - 1
EP - 15
JO - Leibniz International Proceedings in Informatics
JF - Leibniz International Proceedings in Informatics
SN - 1868-8969
M1 - 33
ER -