Mobility Reading Group

Zooid: A DSL for Certified Multiparty Computation

David CASTRO-PEREZ, Francisco FERREIRA, Lorenzo GHERI, Nobuko YOSHIDA

42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021). p. 237 - 251

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.

Paper Paper (fullversion) Electronic version via DOI

BibTeX
Short
Long

@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 = {237--251},
  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 = {237--251},
  publisher = {ACM},
  doi = "10.1145/3453483.3454041",
  year = 2021
}