Formalising a turing-complete choreographic language in Coq

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

1 Downloads (Pure)

Abstract

The 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, its basic properties, Kleene's theory of partial recursive functions, the encoding of these functions as choreographies, and a proof that this encoding is 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.

Original languageEnglish
Title of host publication12th International Conference on Interactive Theorem Proving (ITP 2021)
EditorsLiron Cohen, Cezary Kaliszyk
Volume193
PublisherSchloss Dagstuhl-Leibniz-Zentrum fuer Informatik
Publication date1. Jun 2021
Pages15:1-15:18
ISBN (Electronic)9783959771887
DOIs
Publication statusPublished - 1. Jun 2021
Event12th International Conference on Interactive Theorem Proving, ITP 2021 - Virtual, Rome, Italy
Duration: 29. Jun 20211. Jul 2021

Conference

Conference12th International Conference on Interactive Theorem Proving, ITP 2021
Country/TerritoryItaly
CityVirtual, Rome
Period29/06/202101/07/2021
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume193
ISSN1868-8969

Bibliographical note

Funding Information:
Work partially supported by Villum Fonden, grant no. 29518.

Publisher Copyright:
© Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti.

Keywords

  • Choreographic Programming
  • Formalisation
  • Turing Completeness

Fingerprint

Dive into the research topics of 'Formalising a turing-complete choreographic language in Coq'. Together they form a unique fingerprint.

Cite this