Abstract | ||
---|---|---|
In Choreographic Programming, a distributed system is programmed by giving a , 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. |
Year | Venue | Keywords |
---|---|---|
2018 | Distributed Computing | Choreographies,Curry–Howard isomorphism,Linear logic,Programming languages |
DocType | Volume | Issue |
Journal | 31 | 1 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Marco Carbone | 1 | 0 | 0.68 |
Fabrizio Montesi | 2 | 0 | 1.35 |
Carsten Schürmann | 3 | 15 | 2.89 |