  Theory of choreographic languages typically includes a number of complex
results that are proved by structural induction. The high number of cases and
the subtle details in some of them lead to long reviewing processes, and
occasionally to errors being found in published proofs. In this work, we take a
published proof of Turing completeness of a choreographic language and
formalise it in Coq. Our development includes formalising the choreographic
language and its basic properties, Kleene's theory of partial recursive
functions, the encoding of these functions as choreographies, and proving this
encoding correct.
  With this effort, we show that theorem proving can be a very useful tool in
the field of choreographic languages: besides the added degree of confidence
that we get from a mechanised proof, the formalisation process led us to a
significant simplification of the underlying theory. Our results offer a
foundation for the future formal development of choreographic languages.
