Paper Info
Title
Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes
Abstract
ABSTRACTWe 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.
Year
DOI
Venue
2021
10.1145/3453483.3454041
PLDI
Keywords
DocType
Citations 
multiparty session types, mechanisation, Coq, concurrent processes, protocol compliance, deadlock freedom, liveness
Conference
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
David Castro-Perez100.34
Francisco Ferreira2104.19
Lorenzo Gheri300.34
Nobuko Yoshida462.52