Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes
File(s)main.pdf (770.26 KB)
Accepted version
Author(s)
Castro-Perez, David
Ferreira Ruiz, Francisco
Gheri, Lorenzo
Yoshida, Nobuko
Type
Conference Paper
Abstract
We design and implement Zooid, a domain specific language for certified multiparty communication, embedded in Coq and implemented atop our mechanisation frame work 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.
Date Issued
2021-06-19
Date Acceptance
2021-03-24
Citation
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2021, pp.237-251
ISBN
9781450383912
Publisher
Association for Computing Machinery (ACM)
Start Page
237
End Page
251
Journal / Book Title
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Copyright Statement
© 2021 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, June 2021 Pages 237–251; https://doi.org/10.1145/3453483.3454041
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
The National Cyber Security Centre (NCSC)
Grant Number
EP/T006544/1
EP/K011715/1
ERI 025567 (EP/K034413/1)
PO 20131167
EP/L00058X/1, PO 20131167
EP/N027833/1
PO 20263116
EP/T014709/1
EP/V000462/1
PO 20257975
4214176 / RFA 20601
Source
PLDI 2021
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
multiparty session types
mechanisation
Coq
concurrent processes
protocol compliance
deadlock freedom
liveness
Publication Status
Published
Start Date
2021-06-20
Finish Date
2021-06-26
Coverage Spatial
Virtual
Date Publish Online
2021-06-18