Name
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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1007/978-3-030-85315-0_8 | THEORETICAL ASPECTS OF COMPUTING, ICTAC 2021 |
Keywords | DocType | Volume |
Choreographic programming, Formalisation, Compilation | Conference | 12819 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Luís Cruz-Filipe | 1 | 0 | 0.34 |
| Fabrizio Montesi | 2 | 401 | 30.94 |
| Marco Peressotti | 3 | 32 | 8.48 |