Multiparty Session Types as Coherence Proofs

Marco Carbone, Fabrizio Montesi, Carsten Schürmann, Nobuko Yoshida

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

92 Downloads (Pure)

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.
Original languageEnglish
Title of host publication26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015
EditorsLuca Aceto, David de Frutos Escrig
Publication date2015
Pages412-426
ISBN (Electronic)978-3-939897-91-0
DOIs
Publication statusPublished - 2015
Event26th International Conference on Concurrency Theory - Madrid, Spain
Duration: 1. Sept 20154. Sept 2015

Conference

Conference26th International Conference on Concurrency Theory
Country/TerritorySpain
CityMadrid
Period01/09/201504/09/2015
SeriesLeibniz International Proceedings in Informatics
Volume42
ISSN1868-8969

Keywords

  • Linear Logic
  • Programming languages
  • Session types
  • Type systems

Fingerprint

Dive into the research topics of 'Multiparty Session Types as Coherence Proofs'. Together they form a unique fingerprint.

Cite this