MAG$\pi$ is a Multiparty, Asynchronous and Generalised $\pi$-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$\pi$!, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). Replication is a standard $\pi$-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.
翻译:MAG$\pi$是一种多参与者、异步且泛化的$\pi$演算,通过在会话类型中引入超时机制来对易失通信进行推理。其类型系统保证所有可能的消息丢失均由超时分支处理。在本文中,我们认为这一要求过于严格。我们提出MAG$\pi$!扩展,这是首次将复制引入多参与者会话类型(MPST)的工作。复制是$\pi$演算中用于建模无限可用服务器的标准构造。我们将这一构造提升至类型层面,并证明其简化了分布式客户端-服务器交互的规范。我们证明了与泛化MPST相关的性质:主体归约、会话保真度以及进程属性验证。