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

University of Southern Denmark

Research output: Journal Article or Conference Article in Journal › Conference article › 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
Journal	Lecture Notes in Computer Science
Pages (from-to)	115-133
Number of pages	19
DOIs	https://doi.org/10.1007/978-3-030-85315-0_8
Publication status	Published - 2021
Event	International Colloquium on Theoretical Aspects of Computing - Virtual Event, Nur-Sultan, Kazakhstan Duration: 8 Sept 2021 → 10 Sept 2021 Conference number: 18 https://dblp.org/db/conf/ictac/index.html

Conference

Conference	International Colloquium on Theoretical Aspects of Computing
Number	18
Location	Virtual Event
Country/Territory	Kazakhstan
City	Nur-Sultan
Period	08/09/2021 → 10/09/2021
Internet address	https://dblp.org/db/conf/ictac/index.html

Keywords

Choreographic programming
Compilation
Formalisation

Access to Document

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

Cite this

@inproceedings{2732e43fe7be448dbd091d7088b101ff,

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; International Colloquium on Theoretical Aspects of Computing, ICTAC ; Conference date: 08-09-2021 Through 10-09-2021",

year = "2021",

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

language = "English",

pages = "115--133",

journal = "Lecture Notes in Computer Science",

url = "https://dblp.org/db/conf/ictac/index.html",

}

TY - GEN

T1 - Certifying Choreography Compilation

AU - Cruz-Filipe, Luís

AU - Montesi, Fabrizio

AU - Peressotti, Marco

N1 - Conference code: 18

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 - Conference article

SP - 115

EP - 133

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - International Colloquium on Theoretical Aspects of Computing

Y2 - 8 September 2021 through 10 September 2021

ER -

Certifying Choreography Compilation

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this