Encoding Choice and Replication in 𝚛𝚘𝚕𝚕-Π

Reversible process calculi, such as 𝚛𝚘𝚕𝚕-π , can accommodate fault-tolerant communication protocols. However, untyped process calculi cannot guarantee desirable behavioural properties such as deadlock-freedom. Concomitantly, Multiparty Session Types (MPST) can provide such guarantees by construction, but often do not consider failures. This suggests that, by leveraging both MPST and 𝚛𝚘𝚕𝚕-π , we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, 𝚛𝚘𝚕𝚕-π lacks choice and replication primitives, which are key features for an MPST-based type system. Nonetheless, its expressiveness allows these constructs to be encoded directly. In this paper, we introduce 𝚛𝚘𝚕𝚕-π !⊕ , a variant of 𝚛𝚘𝚕𝚕-π that incorporates choice and replication, and outline its encoding in 𝚛𝚘𝚕𝚕-π . This extension lays the foundation for integrating 𝚛𝚘𝚕𝚕-π with MPST.