MobilityReadingGroup

Implementing Multiparty Session Types in Rust

Nicolas LAGAILLARDIE, Rumyana NEYKOVA, Nobuko YOSHIDA

Multiparty Session Types (MPST) is a typing discipline for communication protocols, which ensures communication safety and deadlock-freedom for more than two participants. This paper reports our on-going research project, implementing multiparty session types in Rust. Current Rust implementations of session types are limited to binary (two-party communications) and introduce errors due to a gap between affinity in Rust and linearity in the session types discipline. To achieve our goal by overcoming these limitations, we extend an existing library for the binary session types to MPST. We created an environment involving a server and clients, communicating through an MQTT (MQ Telemetry Transport) broker with protocols that have been checked by our library.

@inproceedings{LNY2020,
  author = {Nicolas Lagaillardie and Rumyana Neykova and Nobuko Yoshida},
  title = {{Implementing Multiparty Session Types in Rust}},
  booktitle = {12th Workshop on Programming Language Approaches to Concurrency & Communication-cEntric Software},
  pages = {1--8},
  year = 2020
}

@inproceedings{LNY2020,
  author = {Nicolas Lagaillardie and Rumyana Neykova and Nobuko Yoshida},
  title = {{Implementing Multiparty Session Types in Rust}},
  booktitle = {12th Workshop on Programming Language Approaches to Concurrency & Communication-cEntric Software},
  pages = {1--8},
  year = 2020
}