Propositions in Linear Multirole Logic as Multiparty Session Types

TL;DR

This paper introduces linear multirole logic (LMRL), a new logic that generalizes classical linear logic, and demonstrates its properties and applications to multiparty session types and process communication.

Contribution

It formalizes LMRL, proves multi-cut elimination, and establishes a correspondence between process communication and multi-cut elimination in LMRL.

Findings

Multi-cut elimination extends Gentzen's cut-elimination to multiple sequents.

A variant of $alculus for multiparty sessions is developed.

Process communication in the calculus corresponds to multi-cut elimination.

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 $\pi$-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.