2026-08-14T17:51:50Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6181 2024-03-06T10:38:31Z ddc:004 open_access

Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types Carbone, Marco Lindley, Sam Montesi, Fabrizio Schürmann, Carsten Wadler, Philip Multiparty Session Types Linear Logic Propositions as Types 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Marco Carbone and Sam Lindley and Fabrizio Montesi and Carsten Schürmann and Philip Wadler 2016 Is Part Of LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2016.33 urn:nbn:de:0030-drops-61811 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.33 eng https://creativecommons.org/licenses/by/3.0/legalcode