ITU

Choreographies, Logically

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Standard

Choreographies, Logically. / Carbone, Marco; Montesi, Fabrizio; Schürmann, Carsten.

In: Lecture Notes in Computer Science, Vol. 8704, 2014, p. 47-62.

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@inproceedings{35a5f0b15ec14d23a20913884ca228e2,
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",
language = "English",
volume = "8704",
pages = "47--62",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer",

}

RIS

TY - GEN

T1 - Choreographies, Logically

AU - Carbone, Marco

AU - Montesi, Fabrizio

AU - Schürmann, Carsten

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.

M3 - Conference article

VL - 8704

SP - 47

EP - 62

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -

ID: 79278684