Formalising a turing-complete choreographic language in Coq

Publikation: Kapitel i bog/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

1 Downloads (Pure)

Abstrakt

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.

OriginalsprogEngelsk
Titel12th International Conference on Interactive Theorem Proving (ITP 2021)
RedaktørerLiron Cohen, Cezary Kaliszyk
Vol/bind193
ForlagSchloss Dagstuhl-Leibniz-Zentrum fuer Informatik
Publikationsdato1. jun. 2021
Sider15:1-15:18
ISBN (Elektronisk)9783959771887
DOI
StatusUdgivet - 1. jun. 2021
Begivenhed12th International Conference on Interactive Theorem Proving, ITP 2021 - Virtual, Rome, Italien
Varighed: 29. jun. 20211. jul. 2021

Konference

Konference12th International Conference on Interactive Theorem Proving, ITP 2021
Land/OmrådeItalien
ByVirtual, Rome
Periode29/06/202101/07/2021
NavnLeibniz International Proceedings in Informatics, LIPIcs
Vol/bind193
ISSN1868-8969

Bibliografisk note

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

Fingeraftryk

Dyk ned i forskningsemnerne om 'Formalising a turing-complete choreographic language in Coq'. Sammen danner de et unikt fingeraftryk.

Citationsformater