Conference item
Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 770.6KB, Terms of use)
-
- Publisher copy:
- 10.1145/3453483.3454041
Authors
+ Engineering and Physical Sciences Research Council
More from this funder
- Grant:
- EP/N027833/1
- EP/T006544/1
- EP/T014709/1
- 309899
- EP/N028201/1 - 72043/2
- EP/X015955/1 - 316931
- Publisher:
- Association for Computing Machinery
- Host title:
- Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021)
- Pages:
- 237-251
- Publication date:
- 2021-06-18
- Acceptance date:
- 2021-02-25
- Event title:
- 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021)
- Event website:
- https://sigplan.org/OpenTOC/pldi21.html
- Event start date:
- 2021-06-20
- Event end date:
- 2021-06-25
- DOI:
- ISBN:
- 9781450383912
- Language:
-
English
- Keywords:
- Pubs id:
-
1310425
- Local pid:
-
pubs:1310425
- Deposit date:
-
2024-02-27
Terms of use
- Copyright holder:
- Castro-Perez et al
- Copyright date:
- 2021
- Rights statement:
- © 2021 Copyright held by the owner/author(s). Publication rights licensed to ACM.
- Notes:
- This paper was presented at the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021), 20th-25th June 2021. This is the accepted manuscript version of the article. The final version is available online from Association for Computing Machinery at https://dx.doi.org/10.1145/3453483.3454041
If you are the owner of this record, you can report an update to it here: Report update to this record