Certifying Choreography Compilation

Luís Cruz-Filipe*, Fabrizio Montesi, Marco Peressotti

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2021 : 18th International Colloquium
EditorsAntonio Cerone, Peter Csaba Olveczky
PublisherSpringer Science+Business Media
Publication date2021
ISBN (Print)9783030853143
Publication statusPublished - 2021
Event18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 - Virtual, Online
Duration: 8. Sep 202110. Sep 2021


Conference18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021
CityVirtual, Online
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12819 LNCS

Bibliographical note

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.


  • Choreographic programming
  • Compilation
  • Formalisation


Dive into the research topics of 'Certifying Choreography Compilation'. Together they form a unique fingerprint.

Cite this