Multirole Logic

Author: Hongwei Xi and Hanwen Wu

© 2016-2018 Hongwei Xi and Hanwen Wu, All Rights Reserved.

We identify multirole logic as a new form of logic in which conjunction/disjunction is interpreted as an ultrafilter on the power set of some underlying set (of roles) and the notion of negation is generalized to endomorphisms on this underlying set. We formalize both multirole logic (MRL) and linear multirole logic (LMRL) as natural generalizations of classical logic (CL) and classical linear logic (CLL), respectively, and also present a filter-based interpretation for intuitionism in multirole logic. 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.

Papers

• Hanwen Wu, Hongwei Xi. Implementing Linking in Multiparty Sessions, AGERE! (2018).
• Hanwen Wu, Hongwei Xi. Multiparty Dependent Session Types (Extended Abstract), arXiv (2018).
• Hongwei Xi, Hanwen Wu. Multirole Logic and Multiparty Channels, Recent Advances in Concurrency and Logic (2017).
• Hongwei Xi, Hanwen Wu. Multirole Logic, Logic Colloquium (2017).
• Hanwen Wu, Hongwei Xi. Dependent Session Types, arXiv (2017)
• Hongwei Xi, Hanwen Wu. Multirole Logic (Extended Abstract), arXiv (2017)
• Hongwei Xi, Hanwen Wu. Propositions in Linear Multirole Logic as Multiparty Session Types (arXiv 2016 v1, 2017 v2)
• Hongwei Xi, Hanwen Wu. Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions, arXiv (2016)
• Hongwei Xi, Zhiqiang Ren, Hanwen Wu, William Blair. Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus, arXiv (2016)

Talks

The following talk was given by Hanwen Wu at IBM PL Day 2017 hosted by IBM T.J. Watson Research Center. (Dec 4. 2017)

The following talk was given by Hongwei Xi and Hanwen Wu at LC 2017. (Aug 18, 2017)

A version with speaker’s notes can be found here on Scribd.

The following talk was given by Hanwen Wu at NEPLS 2016 hosted by UMass Amherst. (May 31, 2016)

The following talk was given by Hanwen Wu at NEPLS 2015 hosted by Tufts University. (Nov 10, 2015)

It’s code can be found here which also includes a simple encoding of ConcurrentML.

Full Proofs

These proofs are formulated and checked in an older version of ATS and z3.¹ We recommend that you verify one proof at a time and comment out others to make it possible to verify within resource limit.

• Conjunctive Propositional Classical, https://glot.io/snippets/eel70kauxc
• Disjuctive Propositional Classical, https://glot.io/snippets/eel78s1dnm
• Propositional Dual Classical, https://glot.io/snippets/eel4cuqav8
• Propositional Classical Linear, https://glot.io/snippets/eel75yn540

Implementations

Our work has enabled several implementations. The session API formulation is done in Applied Type System. After type checking, it will be compiled into a target language. Currently we experimented several such targets, including C, JavaScript, and Elixir/Erlang.

• ATS/C. This is the first implementation of multiparty dependent session types that supports multiparty linking. The implementation uses a blackboard approach. See our AGERE! WIP paper describing the detail of linking.

• ATS/Elixir, ATS/Erlang. This repo contains several async message-passing implementation on top of the ErlangVM, covering binary sessions, naive multiparty sessions, and multiparty sessions based on LMRL in a different branch. We are currently working on re-organising the code base. The dependent folder contains the latest (as of April 2017) implementation of dependent session types.

• ATS/C. Repo 1 and repo 2 are two implementations of binary session types and multiparty session types, respectively. They are described in Hongwei Xi, Hanwen Wu. Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions (2016). You can also find them on npm, binary and npm, multiparty.

• ATS/Erlang.

Other Resources

• Two tutorials from the series Effective ATS.
• ATS Official Website, http://www.ats-lang.org
• Active Google Groups for discussions, ats-lang-users, ats-lang-club (invite only)