Multiparty session types as coherence proofs
File(s)
Accepted version
Author(s)
Carbone, M
Montesi, F
Schürmann, C
Yoshida, N
Type
Journal Article
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.
Date Issued
2016-11-16
Date Acceptance
2016-11-04
Citation
Acta Informatica, 2016, 54 (3), pp.243-269
ISSN
0001-5903
Start Page
243
End Page
269
Journal / Book Title
Acta Informatica
Volume
54
Issue
3
Copyright Statement
© Springer-Verlag Berlin Heidelberg 2016. The final publication is available at Springer via http://dx.doi.org/10.1007/s00236-016-0285-y
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
Subjects
Science & Technology
Technology
Computer Science, Information Systems
Computer Science
LINEAR LOGIC
Computation Theory & Mathematics
0803 Computer Software
0804 Data Format
0802 Computation Theory And Mathematics
Publication Status
Published