Un-projectable Global Types for Multiparty Sessions

A well-formed global type describes the interaction protocol of multiple end-points via the projection to local specifications. Typed sessions of processes enjoy good communication properties and their overall behaviour is the one described by the global type. We show that a projectable global type is bounded (also said “balanced” in the literature) but also that projectability is not necessary for a global type to be a sound description of well-behaved systems. By revising the semantics of global types via a coinductively defined LTS, we obtain a conservative extension of previous type systems in case of simple sessions without channels and local types, which we call Simple MultiParty Sessions, accommodating unbounded and hence un-projectable global types. Such a system is sound and encompasses infinite sessions that do not type-check for any bounded and/or projectable global type.