@inproceedings{e5e8e1ee88f24ac5a41814b002503343,
title = "Coherence generalises duality: A logical explanation of multiparty session types",
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.",
keywords = "Linear logic, Multiparty session types, Propositions as types",
author = "Marco Carbone and Sam Lindley and Fabrizio Montesi and Carsten Sch{\"u}rmann and Philip Wadler",
year = "2016",
month = aug,
day = "24",
doi = "10.4230/LIPIcs.CONCUR.2016.33",
language = "English",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
editor = "Josee Desharnais and Radha Jagadeesan",
booktitle = "27th International Conference on Concurrency Theory (CONCUR 2016)",
note = "27th International Conference on Concurrency Theory 2016, CONCUR 2016 ; Conference date: 23-08-2016 Through 26-08-2016",
}