Choreographies, Logically
- ,
- Fabrizio Montesi,
- ,
- University of Southern Denmark
Research Output:
Journal Article or Conference Article in Journal
Conference article
Peer-reviewPublication Information
Output type
Research Output:
Journal Article or Conference Article in Journal
Conference article
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 47-62 (15 pages)Journal (Volume, Issue Number)
Lecture Notes in Computer Science (Volume 8704)Publication milestones
- Published - 2014
Publication status
Published - 2014
ISSN
0302-9743Publication IDs
- Scopus: 84906772581
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.
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.
Publication metrics
PlumX
Captures
2
Citations
19