MAG$\pi$!: The Role of Replication in Typing Failure-Prone Communication
<|reference_start|>MAG$\pi$!: The Role of Replication in Typing Failure-Prone Communication: 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.<|reference_end|>
@article{brun2024mag$\pi$!:,
    title={MAG$\pi$!: The Role of Replication in Typing Failure-Prone Communication},
    author={Matthew Alan Le Brun and Ornela Dardha},
    journal={arXiv preprint arXiv:2404.16213},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.16213},
    primaryClass={cs.PL}
}