On Projections of Global Types in Partially Commutative Multiparty Asynchronous Sessions

A theory of multiparty sessions is presented in this paper, where the semantic analysis of global types ensures that the projection onto each participant preserves a strong fairness assumption, i.e., no participant of multiparty sessions will wait for messages that are never sent or will send messages that no other participant will receive. In addition, once a global type is agreed upon by all participants involved, a local protocol from each local viewpoint will be generated as a projection onto each participant using a top-down approach. Furthermore, the introduction of asynchronous communication sub typing allows permutation of actions to raise efficiency, where each local type can be locally refined using our action asynchronous sub typing rules for both dependent and independent messages, which gives a more optimized protocol.