Zooid: a DSL for Certified Multiparty Computation

TL;DR

Zooid is a domain-specific language embedded in Coq that enables certified multiparty communication with verified properties like deadlock freedom and protocol compliance, based on asynchronous multiparty session types.

Contribution

It introduces Zooid, the first mechanised framework for certified multiparty communication with a verified semantics and process language in Coq.

Findings

Provides a fully mechanised metatheory for global and local types

Ensures deadlock freedom, protocol compliance, and liveness guarantees

First implementation of asynchronous multiparty session types in Coq

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.