2024/04/24 by Matthew Alan Le Brun, Brun, Matthew Alan Le, Ornela Dardha +1
Computer Science · #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2404.16213
openalex publication_date 2024/04/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.