Certifying Choreography Compilation

Luís Cruz-Filipe; Fabrizio Montesi; Marco Peressotti

doi:10.1007/978-3-030-85315-0_8

Certifying Choreography Compilation

Luís Cruz-Filipe^*, Fabrizio Montesi, Marco Peressotti

^*Corresponding author for this work

Department of Mathematics and Computer Science

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

Abstract

Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.

Original language	English
Title of host publication	Theoretical Aspects of Computing – ICTAC 2021 : 18th International Colloquium
Editors	Antonio Cerone, Peter Csaba Olveczky
Publisher	Springer Science+Business Media
Publication date	2021
Pages	115-133
ISBN (Print)	9783030853143
DOIs	https://doi.org/10.1007/978-3-030-85315-0_8
Publication status	Published - 2021
Event	18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 - Virtual, Online Duration: 8. Sept 2021 → 10. Sept 2021

Conference

Conference	18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021
City	Virtual, Online
Period	08/09/2021 → 10/09/2021

Series	Lecture Notes in Computer Science
Volume	12819 LNCS
ISSN	0302-9743

Bibliographical note

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.

Keywords

Choreographic programming
Compilation
Formalisation

Documents & Links

10.1007/978-3-030-85315-0_8

https://arxiv.org/pdf/2102.10698

1 Journal article

A Formal Theory of Choreographic Programming
Cruz-Filipe, L., Montesi, F. & Peressotti, M., May 2023, In: Journal of Automated Reasoning. 67, 2, 34 p., 21.
Research output: Contribution to journal › Journal article › Research › peer-review

Open Access
File
42 Downloads (Pure)

A Formal Theory of Choreographic Programming in Coq
Cruz-Filipe, L. (Creator), Montesi, F. (Creator) & Peressotti, M. (Creator), Zenodo, 5. Sept 2022
DOI: 10.5281/zenodo.7773479, https://zenodo.org/record/7773479
Dataset

Cite this

@inproceedings{cc9a18dc41314e3580ffa2c758573baf,

title = "Certifying Choreography Compilation",

abstract = "Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.",

keywords = "Choreographic programming, Compilation, Formalisation",

author = "Lu{\'i}s Cruz-Filipe and Fabrizio Montesi and Marco Peressotti",

note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 ; Conference date: 08-09-2021 Through 10-09-2021",

year = "2021",

doi = "10.1007/978-3-030-85315-0_8",

language = "English",

isbn = "9783030853143",

series = "Lecture Notes in Computer Science",

publisher = "Springer Science+Business Media",

pages = "115--133",

editor = "Antonio Cerone and Olveczky, {Peter Csaba}",

booktitle = "Theoretical Aspects of Computing – ICTAC 2021",

address = "United States",

}

Cruz-Filipe, L , Montesi, F & Peressotti, M 2021, Certifying Choreography Compilation. in A Cerone & PC Olveczky (eds), Theoretical Aspects of Computing – ICTAC 2021 : 18th International Colloquium. Springer Science+Business Media, Lecture Notes in Computer Science, vol. 12819 LNCS, pp. 115-133, 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021, Virtual, Online, 08/09/2021. https://doi.org/10.1007/978-3-030-85315-0_8

Certifying Choreography Compilation. / Cruz-Filipe, Luís ; Montesi, Fabrizio ; Peressotti, Marco.
Theoretical Aspects of Computing – ICTAC 2021 : 18th International Colloquium. ed. / Antonio Cerone; Peter Csaba Olveczky. Springer Science+Business Media, 2021. p. 115-133 (Lecture Notes in Computer Science, Vol. 12819 LNCS).

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

TY - GEN

T1 - Certifying Choreography Compilation

AU - Cruz-Filipe, Luís

AU - Montesi, Fabrizio

AU - Peressotti, Marco

PY - 2021

Y1 - 2021

N2 - Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.

AB - Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.

KW - Choreographic programming

KW - Compilation

KW - Formalisation

U2 - 10.1007/978-3-030-85315-0_8

DO - 10.1007/978-3-030-85315-0_8

M3 - Article in proceedings

AN - SCOPUS:85115182661

SN - 9783030853143

T3 - Lecture Notes in Computer Science

SP - 115

EP - 133

BT - Theoretical Aspects of Computing – ICTAC 2021

A2 - Cerone, Antonio

A2 - Olveczky, Peter Csaba

PB - Springer Science+Business Media

T2 - 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021

Y2 - 8 September 2021 through 10 September 2021

ER -

Certifying Choreography Compilation

Abstract

Conference

Bibliographical note

Keywords

Documents & Links

Fingerprint

Related research output

A Formal Theory of Choreographic Programming

Related datasets

A Formal Theory of Choreographic Programming in Coq

Cite this