Sound and Complete Projection for Global Types

Multiparty session types (MPST) is a typing discipline for specifying the communication patterns that interacting processes must adhere to during an execution. Using an Alice-Bob notation, often referred to as choreographies, the programmer can specify who has to communicate with who at each point in time, also accounting for branching possibilities. In MPST this choreography is called a global type. An operation that is necessary when dealing with global types (and choreographies in general) is that of projection. This is a partial function that given a global type and a participant then attempts to erase all details of the global type irrelevant for this participant. The operation will only be defined for a class of good protocols known as projectable global types. To support repeating protocols, global types allow tail recursion which gives rise to an interpretation of global types as infinite (but regular) trees.

Recent work has taken a relational approach to projection, defining it as a coinductive relation on these regular trees. This definition is well known to be strictly more general than its computable counterpart. In our work we show that one can define the partial function such that it is equally as permissive as the coinductive relation. With respect to the coinductive relation we prove soundness and completeness of projection and explain the design of the procedure. All results have been mechanised in the Coq proof assistant.