2 Search Results for "Sch�rmann, Carsten"


Document
Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types

Authors: Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)


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.

Cite as

Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 33:1-33:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{carbone_et_al:LIPIcs.CONCUR.2016.33,
  author =	{Carbone, Marco and Lindley, Sam and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Wadler, Philip},
  title =	{{Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{33:1--33:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.33},
  URN =		{urn:nbn:de:0030-drops-61811},
  doi =		{10.4230/LIPIcs.CONCUR.2016.33},
  annote =	{Keywords: Multiparty Session Types, Linear Logic, Propositions as Types}
}
Document
Multiparty Session Types as Coherence Proofs

Authors: Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
We propose a Curry-Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.

Cite as

Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty Session Types as Coherence Proofs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 412-426, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{carbone_et_al:LIPIcs.CONCUR.2015.412,
  author =	{Carbone, Marco and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Yoshida, Nobuko},
  title =	{{Multiparty Session Types as Coherence Proofs}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{412--426},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.412},
  URN =		{urn:nbn:de:0030-drops-53661},
  doi =		{10.4230/LIPIcs.CONCUR.2015.412},
  annote =	{Keywords: Programming languages, Type systems, Session Types, Linear Logic}
}
  • Refine by Author
  • 2 Carbone, Marco
  • 2 Montesi, Fabrizio
  • 2 Schürmann, Carsten
  • 1 Lindley, Sam
  • 1 Wadler, Philip
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 Linear Logic
  • 1 Multiparty Session Types
  • 1 Programming languages
  • 1 Propositions as Types
  • 1 Session Types
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2015
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail