Skip to main content
Kent Academic Repository

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)

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 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: https://kar.kent.ac.uk/id/eprint/88249 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.