Propositions in linear multirole logic as multiparty session types

Files
1611.08888v1.pdf(236.19 KB)
First author draft
Date
2016
DOI
Authors
Xi, Hongwei
Wu, Hanwen
Version
First author draft
OA Version
Citation
H. Xi, H. Wu. "Propositions in Linear Multirole Logic as Multiparty Session Types." https://arxiv.org/abs/1611.08888.
Abstract
We identify multirole logic as a new form of logic and formalize linear multirole logic (LMRL) as a natural generalization of classical linear logic (CLL). Among various meta-properties established for LMRL, we obtain one named multi-cut elimination stating that every cut between three (or more) sequents (as a generalization of a cut between two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen. We also present a variant of 𝜋-calculus for multiparty sessions that demonstrates a tight correspondence between process communication in this variant and multi-cut elimination in LMRL, thus extending some recent results by Caires and Pfenning (2010) and Wadler (2012), among others, along a similar line of work.
Description
License