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

Syddansk Universitet

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Konferenceartikel › Forskning › 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.

Originalsprog	Engelsk
Tidsskrift	Lecture Notes in Computer Science
Sider (fra-til)	115-133
Antal sider	19
DOI	https://doi.org/10.1007/978-3-030-85315-0_8
Status	Udgivet - 2021
Begivenhed	International Colloquium on Theoretical Aspects of Computing - Virtual Event, Nur-Sultan, Kasakhstan Varighed: 8 sep. 2021 → 10 sep. 2021 Konferencens nummer: 18 https://dblp.org/db/conf/ictac/index.html

Konference

Konference	International Colloquium on Theoretical Aspects of Computing
Nummer	18
Lokation	Virtual Event
Land/Område	Kasakhstan
By	Nur-Sultan
Periode	08/09/2021 → 10/09/2021
Internetadresse	https://dblp.org/db/conf/ictac/index.html

Adgang til dokumentet

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

Citationsformater

@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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater