Abstract Replication is an alternative construct to recursion for describing infinite behaviours in the $$\pi $$ π -calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce $$\textsf {MPST!} $$ MPST ! , a session-typed multiparty process calculus with replication and first-class roles. We show that replication is not an equivalent alternative to recursion in MPST, and that using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that support mutual exclusion and races. We demonstrate the expressiveness of $$\textsf {MPST!} $$ MPST ! on examples including binary tree serialisation, dining philosophers, and a model of an auction, and explore the implications of replication on the decidability of typechecking.

Abstract Multiparty Session Types(MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several works have emerged which model failures and introduce fault-tolerance techniques. However, such works often make assumptions on the underlying network,e.g., assuming TCP-based communication where messages are guaranteed to be delivered; or adopting centralised reliable nodes and ad-hoc notions of reliability; or only addressing a single kind of failure, such as node crashes. In this work, we develop MAG $$\pi $$ π —a Multiparty, Asynchronous and Generalised $$\pi $$ π -calculus, which is thefirst language and type systemto accommodate in unison: (i) the widest range of non-Byzantine faults, includingmessage loss, delaysandreordering;crashandlink failures; andnetwork partitioning; (ii) a novel and most general notion ofreliability, taking into account the viewpoint ofeachparticipant in the protocol; (iii) a spectrum of network assumptions from the lowest UDP-based network programming to the TCP-based application level. We prove subject reduction and session fidelity; process properties (deadlock freedom, termination,etc.); failure-handling safety and reliability adherence.