Keep me out of the loop: a more flexible choreographic projection

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


Choreographic programming is a paradigm where programmers write global descriptions of distributed protocols, called choreographies, and correct implementations are automatically generated by a mechanism called projection. Not all choreographies are projectable, because decisions made by one process must be communicated to other processes whose behaviour depends on them – a property known as knowledge of choice.
The standard formulation of knowledge of choice disallows protocols such as third-party authentication with retries, where two processes iteratively interact, and other processes wait to be notified at the end of this loop. In this work we show how knowledge of choice can be weakened, extending the class of projectable choreographies with these and other interesting behaviours. The whole development is formalised in Coq. Working with a proof assistant was crucial to our development, because of the help it provided with detecting counterintuitive edge cases that would otherwise have gone unnoticed.
Original languageEnglish
Title of host publicationProceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning : EPiC Series in Computing
Editors Ruzica Piskac, Andrei Voronkov
Number of pages20
PublisherEthnographic Praxis in Industry Conference (EPIC)
Publication date3. Jun 2023
Publication statusPublished - 3. Jun 2023


  • Choreographic Programming
  • Distributed protocols
  • Theorem proving
  • Certified implementation
  • distributed protocols
  • theorem proving


Dive into the research topics of 'Keep me out of the loop: a more flexible choreographic projection'. Together they form a unique fingerprint.

Cite this