References & Citations
Computer Science > Programming Languages
Title: MAG$π$!: The Role of Replication in Typing Failure-Prone Communication
(Submitted on 24 Apr 2024)
Abstract: 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.
Submission history
From: Matthew Alan Le Brun [view email][v1] Wed, 24 Apr 2024 21:21:51 GMT (47kb)
Link back to: arXiv, form interface, contact.