Multiparty Session Types as Coherence Proofs

File Description SizeFormat 
6.pdfPublished version634.34 kBAdobe PDFDownload
Title: Multiparty Session Types as Coherence Proofs
Author(s): Carbone, M
Montesi, F
Schürmann, C
Yoshida, N
Item Type: Conference Paper
Abstract: © Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida; licensed under Creative Commons License CC-BY.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.
Publication Date: 4-Sep-2015
Date of Acceptance: 15-Jun-2015
URI: http://hdl.handle.net/10044/1/34010
DOI: https://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.412
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
Sponsor/Funder: Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Funder's Grant Number: ERI 025567 (EP/K034413/1)
PO 1553380
EP/K011715/1
612985
Conference Name: 26th International Conference on Concurrency Theory (CONCUR 2015)
Publication Status: Published
Start Date: 2015-09-01
Finish Date: 2015-09-04
Conference Place: Madrid, Spain
Open Access location: http://drops.dagstuhl.de/opus/volltexte/2015/5366/pdf/6.pdf
Appears in Collections:Computing



Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons