Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.
|Title of host publication||Theoretical Aspects of Computing – ICTAC 2021 : 18th International Colloquium|
|Editors||Antonio Cerone, Peter Csaba Olveczky|
|Publisher||Springer Science+Business Media|
|Publication status||Published - 2021|
|Event||18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 - Virtual, Online|
Duration: 8. Sep 2021 → 10. Sep 2021
|Conference||18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021|
|Period||08/09/2021 → 10/09/2021|
|Series||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
Bibliographical notePublisher Copyright:
© 2021, Springer Nature Switzerland AG.
- Choreographic programming