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

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review


Choreographic programming is a paradigm where programmers write global descrip- tions of distributed protocols, called choreographies, and correct implementations are au- tomatically generated by a mechanism called projection. Not all choreographies are pro- jectable, 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.
TitelProceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning : EPiC Series in Computing
Redaktører Ruzica Piskac, Andrei Voronkov
Antal sider20
ForlagEthnographic Praxis in Industry Conference (EPIC)
Publikationsdato3. jun. 2023
StatusUdgivet - 3. jun. 2023


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


Dyk ned i forskningsemnerne om 'Keep me out of the loop: a more flexible choreographic projection'. Sammen danner de et unikt fingeraftryk.