Formalising a Turing-Complete Choreographic Language in Coq

TL;DR

This paper formalises a Turing-complete choreographic language in Coq, demonstrating the usefulness of theorem proving for verifying and simplifying complex properties in choreographic language theory.

Contribution

It provides the first formal proof of Turing completeness for a choreographic language in Coq, including formalisation of the language, its properties, and encoding of recursive functions.

Findings

Formal proof of Turing completeness in Coq

Simplification of the underlying theory through formalisation

Establishment of a foundation for future formal development

Abstract

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.