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

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.