Zooid: a DSL for Certified Multiparty Computation
Programming Languages
2021-03-19 v1
Abstract
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.
Cite
@article{arxiv.2103.10269,
title = {Zooid: a DSL for Certified Multiparty Computation},
author = {David Castro-Perez and Francisco Ferreira and Lorenzo Gheri and Nobuko Yoshida},
journal= {arXiv preprint arXiv:2103.10269},
year = {2021}
}