Multiparty Session Types as Coherence Proofs
File(s)
Published version
Author(s)
Carbone, M
Montesi, F
Schürmann, C
Yoshida, N
Type
Conference Paper
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.
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.
Date Issued
2015-09-04
Date Acceptance
2015-06-15
Citation
26th International Conference on Concurrency Theory (CONCUR 2015)., 2015, pp.412-426
Publisher
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing
Start Page
412
End Page
426
Journal / Book Title
26th International Conference on Concurrency Theory (CONCUR 2015).
Copyright Statement
© Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida;
licensed under Creative Commons License CC-BY
licensed under Creative Commons License CC-BY
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Grant Number
ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
Source
26th International Conference on Concurrency Theory (CONCUR 2015)
Publication Status
Published
Start Date
2015-09-01
Finish Date
2015-09-04
Coverage Spatial
Madrid, Spain