Abstract
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. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Carbone, M., Montesi, F., & Schürmann, C. (2014). Choreographies, logically. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704 LNCS, pp. 47–62). Springer Verlag. https://doi.org/10.1007/978-3-662-44584-6_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
