MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Certifying Data in Multiparty Session Types
Bernardo TONINHO, Nobuko YOSHIDA
A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (WadlerFest). p. 433 - 458

Multiparty session types (MPST) are a typing discipline for ensuring the coordination and orchestration of multi-agent communication in concurrent and distributed programs. However, by mostly focusing on the communication aspects of concurrency, MPST are often unable to capture important data invariants in programs. In this work we propose to increase the expressiveness of MPST by considering a notion of value dependencies in order to certify invariants of exchanged data in concurrent and distributed settings.

@inproceedings{TY2016,
  author = {Bernardo Toninho and Nobuko Yoshida},
  title = {{Certifying Data in Multiparty Session Types}},
  booktitle = {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday},
  series = {LNCS},
  volume = {9600},
  pages = {433--458},
  publisher = {Springer},
  year = 2016
}
@inproceedings{TY2016,
  author = {Bernardo Toninho and Nobuko Yoshida},
  title = {{Certifying Data in Multiparty Session Types}},
  booktitle = {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday},
  series = {LNCS},
  volume = {9600},
  pages = {433--458},
  publisher = {Springer},
  doi = "10.1007/978-3-319-30936-1_23",
  year = 2016
}