Multirole Logic and Multiparty Channels

TL;DR

This paper introduces multirole logic as a new logical framework generalizing classical and linear logic, with applications to multiparty communication in distributed programming, supported by theoretical foundations and a lambda-calculus implementation.

Contribution

It formalizes multirole logic and linear multirole logic, extending cut-elimination and providing a foundation for multiparty session types in distributed systems.

Findings

Established multiparty cut-elimination property.

Developed a lambda-calculus with multiparty channels based on LMRL.

Provided an ultrafilter interpretation for intuitionistic logic.

Abstract

We identify multirole logic as a new form of logic in which conjunction/disjunction is interpreted as an ultrafilter on some underlying set of roles and the notion of negation is generalized to endomorphisms on this set. We formulate both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively. Among various meta-properties established for MRL and LMRL, we obtain one named multiparty cut-elimination stating that every cut involving one or more sequents (as a generalization of a binary cut involving exactly two sequents) can be eliminated, thus extending the celebrated result of cut-elimination by Gentzen. As a side note, we also give an ultrafilter-based interpretation for intuitionism, formulating MRLJ as a natural generalization of intuitionistic logic (IL). An immediate application of LMRL can be found in a formulation of session types for channels that support multiparty communication in distributed programming. We present a multi-threaded lambda-calculus (MTLC) where threads communicate on linearly typed multiparty channels that are directly rooted in LMRL, establishing for MTLC both type preservation and global progress. The primary contribution of the paper consists of both identifying multirole logic as a new form of logic and establishing a theoretical foundation for it, and the secondary contribution lies in applying multirole logic to the practical domain of distributed programming.