Skip to main content

Zooid: A DSL for Certified Multiparty Computation

Castro-Perez, David, Ferreira, Francisco, Gheri, Lorenzo, Yoshida, Nobuko (2021) Zooid: A DSL for Certified Multiparty Computation. In: PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. . ACM ISBN 978-1-4503-8391-2. (doi:10.1145/3453483.3454041) (KAR id:88249)

PDF Author's Accepted Manuscript
Language: English

Download (861kB) Preview
[thumbnail of main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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 forthe 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.

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1145/3453483.3454041
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: David Castro-Perez
Date Deposited: 18 May 2021 14:14 UTC
Last Modified: 13 Jan 2022 23:12 UTC
Resource URI: (The current URI for this page, for reference purposes)
Castro-Perez, David:
  • Depositors only (login required):


Downloads per month over past year