Choreographies, Logically

Marco Carbone; Fabrizio Montesi; Carsten Schürmann

doi:10.1007/978-3-662-44584-6_5

Choreographies, Logically

Marco Carbone, Fabrizio Montesi, Carsten Schürmann

Department of Mathematics and Computer Science

IT University of Copenhagen

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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.

Original language	English
Title of host publication	CONCUR 2014 – Concurrency Theory : 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings
Editors	Paolo Paldan, Daniele Gorda
Number of pages	16
Publisher	Springer
Publication date	2014
Pages	47-62
ISBN (Print)	978-3-662-44583-9
ISBN (Electronic)	978-3-662-44584-6
DOIs	https://doi.org/10.1007/978-3-662-44584-6_5
Publication status	Published - 2014
Event	International conference, CONCUR 2014 - Rome, Italy Duration: 2. Sept 2014 → 5. Sept 2014 Conference number: 25

Conference

Conference	International conference, CONCUR 2014
Number	25
Country/Territory	Italy
City	Rome
Period	02/09/2014 → 05/09/2014

Series	Lecture Notes in Computer Science
Volume	8704
ISSN	0302-9743

Documents & Links

10.1007/978-3-662-44584-6_5

http://dx.doi.org/10.1007/978-3-662-44584-6_5

Cite this

@inproceedings{e87a3f1beae64ff3861bb87f60273249,

title = "Choreographies, Logically",

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.",

author = "Marco Carbone and Fabrizio Montesi and Carsten Sch{\"u}rmann",

year = "2014",

doi = "10.1007/978-3-662-44584-6_5",

language = "English",

isbn = "978-3-662-44583-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "47--62",

editor = "Paolo Paldan and Daniele Gorda",

booktitle = "CONCUR 2014 – Concurrency Theory",

address = "Germany",

note = "International conference, CONCUR 2014 ; Conference date: 02-09-2014 Through 05-09-2014",

}

Carbone, M, Montesi, F & Schürmann, C 2014, Choreographies, Logically. in P Paldan & D Gorda (eds), CONCUR 2014 – Concurrency Theory : 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. Springer, Lecture Notes in Computer Science, vol. 8704, pp. 47-62, International conference, CONCUR 2014, Rome, Italy, 02/09/2014. https://doi.org/10.1007/978-3-662-44584-6_5

Choreographies, Logically. / Carbone, Marco; Montesi, Fabrizio; Schürmann, Carsten.
CONCUR 2014 – Concurrency Theory : 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings. ed. / Paolo Paldan; Daniele Gorda. Springer, 2014. p. 47-62 (Lecture Notes in Computer Science, Vol. 8704).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Choreographies, Logically

AU - Carbone, Marco

AU - Montesi, Fabrizio

AU - Schürmann, Carsten

N1 - Conference code: 25

PY - 2014

Y1 - 2014

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.

U2 - 10.1007/978-3-662-44584-6_5

DO - 10.1007/978-3-662-44584-6_5

M3 - Article in proceedings

SN - 978-3-662-44583-9

T3 - Lecture Notes in Computer Science

SP - 47

EP - 62

BT - CONCUR 2014 – Concurrency Theory

A2 - Paldan, Paolo

A2 - Gorda, Daniele

PB - Springer

T2 - International conference, CONCUR 2014

Y2 - 2 September 2014 through 5 September 2014

ER -

Choreographies, Logically

Abstract

Conference

Documents & Links

Fingerprint

Cite this