Title
Choreographies, Logically.
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 Carbone100.68
Fabrizio Montesi201.35
Carsten Schürmann3152.89