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.
Andres Erbsen Massachusetts Institute of Technology, Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, Clark Wood Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology
Andres Erbsen Massachusetts Institute of Technology, Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, Clark Wood Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology