Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes
David Castro, Francisco Ferreira, Lorenzo Gheri, Nobuko Yoshida
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.
Topics & Concepts
Computer scienceLivenessAsynchronous communicationProgramming languageCertificationMetatheorySemantics (computer science)Process (computing)Software engineeringTheoretical computer scienceComputer networkLawPolitical scienceLogic, programming, and type systemsFormal Methods in VerificationSecurity and Verification in Computing