Formalising a turing-complete choreographic language in Coq

Luis Cruz-Filipe; Fabrizio Montesi; Marco Peressotti

doi:10.4230/LIPIcs.ITP.2021.15

Formalising a turing-complete choreographic language in Coq

Luis Cruz-Filipe, Fabrizio Montesi, Marco Peressotti

Department of Mathematics and Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

14 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 language	English
Title of host publication	12th International Conference on Interactive Theorem Proving (ITP 2021)
Editors	Liron Cohen, Cezary Kaliszyk
Volume	193
Publisher	Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik
Publication date	1. Jun 2021
Pages	15:1-15:18
ISBN (Electronic)	9783959771887
DOIs	https://doi.org/10.4230/LIPIcs.ITP.2021.15
Publication status	Published - 1. Jun 2021
Event	12th International Conference on Interactive Theorem Proving, ITP 2021 - Virtual, Rome, Italy Duration: 29. Jun 2021 → 1. Jul 2021

Conference

Conference	12th International Conference on Interactive Theorem Proving, ITP 2021
Country/Territory	Italy
City	Virtual, Rome
Period	29/06/2021 → 01/07/2021

Series	Leibniz International Proceedings in Informatics, LIPIcs
Volume	193
ISSN	1868-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

Documents & Links

10.4230/LIPIcs.ITP.2021.15Licence: CC BY

Open Access VersionFinal published version, 654 KBLicence: CC BY

Cite this

Cruz-Filipe, L., Montesi, F., & Peressotti, M. (2021). Formalising a turing-complete choreographic language in Coq. In L. Cohen, & C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving (ITP 2021) (Vol. 193, pp. 15:1-15:18). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Leibniz International Proceedings in Informatics, LIPIcs Vol. 193 https://doi.org/10.4230/LIPIcs.ITP.2021.15

Cruz-Filipe, Luis ; Montesi, Fabrizio ; Peressotti, Marco. / Formalising a turing-complete choreographic language in Coq. 12th International Conference on Interactive Theorem Proving (ITP 2021). editor / Liron Cohen ; Cezary Kaliszyk. Vol. 193 Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2021. pp. 15:1-15:18 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 193).

@inproceedings{f67b2020af4d42279b72dc32a7445a83,

title = "Formalising a turing-complete choreographic language in Coq",

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. ",

keywords = "Choreographic Programming, Formalisation, Turing Completeness",

author = "Luis Cruz-Filipe and Fabrizio Montesi and Marco Peressotti",

note = "Funding Information: Work partially supported by Villum Fonden, grant no. 29518. Publisher Copyright: {\textcopyright} Lu{\'i}s Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti.; 12th International Conference on Interactive Theorem Proving, ITP 2021 ; Conference date: 29-06-2021 Through 01-07-2021",

year = "2021",

month = jun,

day = "1",

doi = "10.4230/LIPIcs.ITP.2021.15",

language = "English",

volume = "193",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik",

pages = "15:1--15:18",

editor = "Liron Cohen and Cezary Kaliszyk",

booktitle = "12th International Conference on Interactive Theorem Proving (ITP 2021)",

}

Cruz-Filipe, L , Montesi, F & Peressotti, M 2021, Formalising a turing-complete choreographic language in Coq. in L Cohen & C Kaliszyk (eds), 12th International Conference on Interactive Theorem Proving (ITP 2021). vol. 193, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Leibniz International Proceedings in Informatics, LIPIcs, vol. 193, pp. 15:1-15:18, 12th International Conference on Interactive Theorem Proving, ITP 2021, Virtual, Rome, Italy, 29/06/2021. https://doi.org/10.4230/LIPIcs.ITP.2021.15

Formalising a turing-complete choreographic language in Coq. / Cruz-Filipe, Luis ; Montesi, Fabrizio ; Peressotti, Marco.

12th International Conference on Interactive Theorem Proving (ITP 2021). ed. / Liron Cohen; Cezary Kaliszyk. Vol. 193 Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2021. p. 15:1-15:18 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 193).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Formalising a turing-complete choreographic language in Coq

AU - Cruz-Filipe, Luis

AU - Montesi, Fabrizio

AU - Peressotti, Marco

N1 - Funding Information: Work partially supported by Villum Fonden, grant no. 29518. Publisher Copyright: © Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti.

PY - 2021/6/1

Y1 - 2021/6/1

N2 - 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.

AB - 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.

KW - Choreographic Programming

KW - Formalisation

KW - Turing Completeness

U2 - 10.4230/LIPIcs.ITP.2021.15

DO - 10.4230/LIPIcs.ITP.2021.15

M3 - Article in proceedings

VL - 193

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 15:1-15:18

BT - 12th International Conference on Interactive Theorem Proving (ITP 2021)

A2 - Cohen, Liron

A2 - Kaliszyk, Cezary

PB - Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik

T2 - 12th International Conference on Interactive Theorem Proving, ITP 2021

Y2 - 29 June 2021 through 1 July 2021

ER -

Cruz-Filipe L , Montesi F , Peressotti M. Formalising a turing-complete choreographic language in Coq. In Cohen L, Kaliszyk C, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021). Vol. 193. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. 2021. p. 15:1-15:18. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 193). doi: 10.4230/LIPIcs.ITP.2021.15

Formalising a turing-complete choreographic language in Coq

Abstract

Conference

Bibliographical note

Keywords

Documents & Links

Fingerprint

Cite this