MAGπ!: The Role of Replication in Typing Failure-Prone Communication

MAGπ is a Multiparty, Asynchronous and Generalised π-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAGπ!, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). Replication is a standard π-calculus construct used to model infinitely available servers. We lift this construct to type-level, and show that it simplifies specification of distributed client-server interactions. We prove properties relevant to generalised MPST: subject reduction, session fidelity and process property verification.