ITU

Multiparty Session Types as Coherence Proofs

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Standard

Multiparty Session Types as Coherence Proofs. / Carbone, Marco; Montesi, Fabrizio; Schürmann, Carsten; Yoshida, Nobuko.

26th International Conference on Concurrency Theory (CONCUR 2015): Leibniz International Proceedings in Informatics. Vol. 42 Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, 2015. p. 412.

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Harvard

Carbone, M, Montesi, F, Schürmann, C & Yoshida, N 2015, Multiparty Session Types as Coherence Proofs. in 26th International Conference on Concurrency Theory (CONCUR 2015): Leibniz International Proceedings in Informatics. vol. 42, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, pp. 412. https://doi.org/10.4230/LIPIcs.CONCUR.2015.412

APA

Carbone, M., Montesi, F., Schürmann, C., & Yoshida, N. (2015). Multiparty Session Types as Coherence Proofs. In 26th International Conference on Concurrency Theory (CONCUR 2015): Leibniz International Proceedings in Informatics (Vol. 42, pp. 412). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. https://doi.org/10.4230/LIPIcs.CONCUR.2015.412

Vancouver

Carbone M, Montesi F, Schürmann C, Yoshida N. Multiparty Session Types as Coherence Proofs. In 26th International Conference on Concurrency Theory (CONCUR 2015): Leibniz International Proceedings in Informatics. Vol. 42. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. 2015. p. 412 https://doi.org/10.4230/LIPIcs.CONCUR.2015.412

Author

Carbone, Marco ; Montesi, Fabrizio ; Schürmann, Carsten ; Yoshida, Nobuko. / Multiparty Session Types as Coherence Proofs. 26th International Conference on Concurrency Theory (CONCUR 2015): Leibniz International Proceedings in Informatics. Vol. 42 Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, 2015. pp. 412

Bibtex

@inproceedings{6fb7e12379104ff983a908680ab15d72,
title = "Multiparty Session Types as Coherence Proofs",
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.",
author = "Marco Carbone and Fabrizio Montesi and Carsten Sch{\"u}rmann and Nobuko Yoshida",
year = "2015",
doi = "10.4230/LIPIcs.CONCUR.2015.412",
language = "English",
volume = "42",
pages = "412",
booktitle = "26th International Conference on Concurrency Theory (CONCUR 2015)",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH",

}

RIS

TY - GEN

T1 - Multiparty Session Types as Coherence Proofs

AU - Carbone, Marco

AU - Montesi, Fabrizio

AU - Schürmann, Carsten

AU - Yoshida, Nobuko

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.4230/LIPIcs.CONCUR.2015.412

DO - 10.4230/LIPIcs.CONCUR.2015.412

M3 - Article in proceedings

VL - 42

SP - 412

BT - 26th International Conference on Concurrency Theory (CONCUR 2015)

PB - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH

ER -

ID: 80607081