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. Sept 202110. Sept 2021


Conference18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021
CityVirtual, Online
SeriesLecture Notes in Computer Science
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