A formal theory of choreographic programming
From MaRDI portal
Abstract: Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of choreographies typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of these proofs has led to important errors being found in published works. In this work, we formalise the theory of a choreographic programming language in Coq. Our development includes the basic properties of this language, a proof of its Turing completeness, a compilation procedure to a process language, and an operational characterisation of the correctness of this procedure. Our formalisation experience illustrates the benefits of using a theorem prover: we get both an additional degree of confidence from the mechanised proof, and a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.
Cites work
- A core model for choreographic programming
- Certifying choreography compilation
- Deadlock-freedom-by-design, multiparty asynchronous global programming
- Discretionary Information Flow Control for Interaction-Oriented Specifications
- Enforcing availability in failure-aware communicating systems
- Formal techniques for distributed objects, components, and systems. 36th IFIP WG 6.1 international conference, FORTE 2016, held as part of the 11th international federated conference on distributed computing techniques, DisCoTec 2016, Heraklion, Crete, Gr
- Foundations of software science and computation structures. 20th international conference, FOSSACS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017. Proceedings
- HOCore in Coq
- scientific article; zbMATH DE number 6703933 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- scientific article; zbMATH DE number 7327953 (Why is no real title available?)
- scientific article; zbMATH DE number 7699432 (Why is no real title available?)
- Multiparty asynchronous session types
- On global types and multi-party sessions
- On the boundary between decidability and undecidability of asynchronous session subtyping
- On the undecidability of asynchronous session subtyping
- Procedural Choreographic Programming
- Session types as intuitionistic linear propositions
- The Paths to Choreography Extraction
- Undecidability of asynchronous session subtyping
- Using encryption for authentication in large networks of computers
Cited in
(11)- A core model for choreographic programming
- Realisability of choreographies
- scientific article; zbMATH DE number 6703933 (Why is no real title available?)
- The Paths to Choreography Extraction
- scientific article; zbMATH DE number 7454921 (Why is no real title available?)
- Procedural Choreographic Programming
- Certified compilation of choreographies with \textsf{hacc}
- Completeness of asynchronous session tree subtyping in Coq
- Keep me out of the loop: a more flexible choreographic projection
- Formalising subject reduction and progress for multiparty session processes
- Formalising asynchronous session subtyping
This page was built for publication: A formal theory of choreographic programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6161233)
