  Programming communicating processes is challenging, because it requires
writing separate programs that perform compatible send and receive actions at
the right time during execution. Leaving this task to the programmer can easily
lead to bugs. Choreographic programming addresses this challenge by equipping
developers with high-level abstractions for codifying the desired communication
structures from a global viewpoint. Given a choreography, implementations of
the involved processes can be automatically generated by endpoint projection
(EPP).
  While choreographic programming prevents manual mistakes in the
implementation of communications, the correctness of a choreographic
programming framework crucially hinges on the correctness of its complex
compiler, which has motivated formalisation of theories of choreographic
programming in theorem provers. In this paper, we build upon one of these
formalisations to construct a toolchain that produces executable code from a
choreography.
