TY - JOUR
T1 - Choreographies, logically
AU - Carbone, Marco
AU - Montesi, Fabrizio
AU - Schürmann, Carsten
PY - 2018
Y1 - 2018
N2 - In Choreographic Programming, a distributed system is programmed by giving a choreography, a global description of its interactions, instead of separately specifying the behaviour of each of its processes. Process implementations in terms of a distributed language can then be automatically projected from a choreography. We present Linear Compositional Choreographies (LCC), a proof theory for reasoning about programs that modularly combine choreographies with processes. Using LCC, we logically reconstruct a semantics and a projection procedure for programs. For the first time, we also obtain a procedure for extracting choreographies from process terms.
AB - In Choreographic Programming, a distributed system is programmed by giving a choreography, a global description of its interactions, instead of separately specifying the behaviour of each of its processes. Process implementations in terms of a distributed language can then be automatically projected from a choreography. We present Linear Compositional Choreographies (LCC), a proof theory for reasoning about programs that modularly combine choreographies with processes. Using LCC, we logically reconstruct a semantics and a projection procedure for programs. For the first time, we also obtain a procedure for extracting choreographies from process terms.
KW - Choreographies
KW - Curry–Howard isomorphism
KW - Linear logic
KW - Programming languages
U2 - 10.1007/s00446-017-0295-1
DO - 10.1007/s00446-017-0295-1
M3 - Journal article
AN - SCOPUS:85014780411
SN - 0178-2770
VL - 31
SP - 51
EP - 67
JO - Distributed Computing
JF - Distributed Computing
IS - 1
ER -