MobilityReadingGroup

Encoding Choice and Replication in roll-π

Adam BARWELL , Ping HOU , Martin VASSOR , Nobuko YOSHIDA

Reversible process calculi, such as roll-π, 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 roll-π, we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, roll-π 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 roll-π!⊕, a variant of roll-π that incorporates choice and replication, and outline its encoding in roll-π. This extension lays the foundation for integrating roll-π with MPST.

@inproceedings{BHVY2025,
  author = {Adam Barwell and Ping Hou and Martin Vassor and Nobuko Yoshida},
  title = {{Encoding Choice and Replication in roll-π}},
  booktitle = {17th Conference on Reversible Computation},
  volume = {15716},
  pages = {27--36},
  publisher = {Lecture Notes in Computer Science (LNCS)},
  year = 2025
}

@inproceedings{BHVY2025,
  author = {Adam Barwell and Ping Hou and Martin Vassor and Nobuko Yoshida},
  title = {{Encoding Choice and Replication in roll-π}},
  booktitle = {17th Conference on Reversible Computation},
  volume = {15716},
  pages = {27--36},
  publisher = {Lecture Notes in Computer Science (LNCS)},
  doi = "10.1007/978-3-031-97063-4_3",
  year = 2025
}