MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Zooid: A DSL for Certified Multiparty Computation
David CASTRO-PEREZ, Francisco FERREIRA, Lorenzo GHERI, Nobuko YOSHIDA
To appear in
42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021)

We design and implement Zooid, a domain specific language for certified multiparty communication, embedded in Coq and implemented atop our mechanisation framework of asynchronous multiparty session types (the first of its kind). Zooid provides a fully mechanised metatheory for the semantics of global and local types, and a fully verified end-point process language that faithfully reflects the type-level behaviours and thus inherits the global types properties such as deadlock freedom, protocol compliance, and liveness guarantees.

@inproceedings{CFGY2021,
  author = {David Castro-Perez and Francisco Ferreira and Lorenzo Gheri and Nobuko Yoshida},
  title = {{Zooid: A DSL for Certified Multiparty Computation}},
  booktitle = {42nd ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages = {--},
  publisher = {ACM},
  year = 2021
}
@inproceedings{CFGY2021,
  author = {David Castro-Perez and Francisco Ferreira and Lorenzo Gheri and Nobuko Yoshida},
  title = {{Zooid: A DSL for Certified Multiparty Computation}},
  booktitle = {42nd ACM SIGPLAN Conference on Programming Language Design and Implementation},
  pages = {--},
  publisher = {ACM},
  year = 2021
}