Applied Choreographies
Saverio Giallorenzo, Fabrizio Montesi, Maurizio Gabbrielli

TL;DR
This paper introduces Applied Choreographies, a formal framework that ensures correct, deadlock-free implementation of choreographies in service-oriented computing by formalising the compilation process from global descriptions to low-level code.
Contribution
It formalises the entire compilation chain from choreographies to SOC implementations, providing correctness guarantees at each stage.
Findings
Formal translation of name-based communication to SOC mechanisms
Projection of choreographies into participant-specific processes
Guarantee of deadlock-free, faithful implementations
Abstract
Choreographic Programming is a correct-by-construction paradigm where a compilation procedure synthesises deadlock-free, concurrent, and distributed communicating processes from global, declarative descriptions of communications, called choreographies. Previous work used choreographies for the synthesis of programs. Alas, there is no formalisation that provides a chain of correctness from choreographies to their implementations. This problem originates from the gap between existing theoretical models, which abstract communications using channel names (\`a la CCS/{\pi}-calculus), and their implementations, which use low-level mechanisms for message routing. As a solution, we propose the theoretical framework of Applied Choreographies. In the framework, developers write choreographies in a language that follows the standard syntax and name-based communication semantics of previous works.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Distributed systems and fault tolerance · Advanced Software Engineering Methodologies
