  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.
