English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

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

Formalising a Turing-Complete Choreographic Language in Coq