Certifying Choreography Compilation
Programming Languages
2021-08-30 v2 Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.2102.10698,
title = {Certifying Choreography Compilation},
author = {Luís Cruz-Filipe and Fabrizio Montesi and Marco Peressotti},
journal= {arXiv preprint arXiv:2102.10698},
year = {2021}
}