Multiparty session types is a typing discipline used to write specifications, known as global types, for branching and recursive message-passing systems. A necessary operation on global types is projection to abstractions of local behaviour, called local types. Typically, this is a computable partial function that given a global type and a role erases all details irrelevant to this role. Computable projection functions in the literature are either unsound or too restrictive when dealing with recursion and branching. Recent work has taken a more general approach to projection defining it as a coinductive, but not computable, relation. Our work defines a new computable projection function that is sound and complete with respect to its coinductive counterpart and, hence, equally expressive. All results have been mechanised in the Coq proof assistant.

This work is part of the ongoing attempt to mechanise in Coq the results of the original paper on Multiparty Asynchronous Session Types. This is joint work with my PhD student (Dawit Tirore) and my colleague (Jesper Bengtson). The results are to appear in the proceedings of the Fourteenth Conference on Interactive Theorem Proving (ITP’23).