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.

翻译：我们提出多角色逻辑作为逻辑的一种新形式，其中合取/析取被解释为某个底层角色集上的超滤子，而否定概念被推广为该集合上的自同态。我们分别将多角色逻辑（MRL）和线性多角色逻辑（LMRL）形式化为经典逻辑（CL）和经典线性逻辑（CLL）的自然推广。在MRL和LMRL建立的若干元性质中，我们得到了一个名为多方 cut-elimination 的性质，它表明涉及一个或多个相继式（作为恰好涉及两个相继式的二元消去规则的推广）的每个 cut 均可被消除，从而扩展了Gentzen著名的 cut-elimination 结果。作为补充，我们还基于超滤子为直觉主义给出了解释，将MRLJ形式化为直觉主义逻辑（IL）的自然推广。LMRL的一个直接应用体现在为分布式编程中支持多方通信的通道制定会话类型。我们提出了一种多线程lambda演算（MTLC），其中线程通过直接根植于LMRL的线性类型化多方通道进行通信，并为MTLC建立了类型保持和全局进展性质。本文的主要贡献在于识别多角色逻辑作为一种新的逻辑形式并为其建立理论基础，次要贡献在于将多角色逻辑应用于分布式编程的实践领域。