  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.
