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

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.

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
Pages115-133
ISBN (Print)9783030853143
DOIs
Publication statusPublished - 2021
Event18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 - Virtual, Online
Duration: 8. Sep 202110. Sep 2021

Conference

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

Bibliographical note

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.

Keywords

  • Choreographic programming
  • Compilation
  • Formalisation

Fingerprint

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

Cite this