Multparty Classical Choreographies
Research output: Contribution to conference - NOT published in proceeding or journal › Paper › Research › peer-review
We present Multiparty Classical Choreographies (MCC), a
language model where global descriptions of communicating systems
(choreographies) implement typed multiparty sessions. Typing is achieved
by generalising classical linear logic to judgements that explicitly record
parallelism by means of hypersequents. Our approach unifies different
lines of work on choreographies and processes with multiparty sessions,
as well as their connection to linear logic. Thus, results developed in one
context are carried over to the others. Key novelties of MCC include
support for server invocation in choreographies, as well as logic-driven
compilation of choreographies with replicated processes.
language model where global descriptions of communicating systems
(choreographies) implement typed multiparty sessions. Typing is achieved
by generalising classical linear logic to judgements that explicitly record
parallelism by means of hypersequents. Our approach unifies different
lines of work on choreographies and processes with multiparty sessions,
as well as their connection to linear logic. Thus, results developed in one
context are carried over to the others. Key novelties of MCC include
support for server invocation in choreographies, as well as logic-driven
compilation of choreographies with replicated processes.
Original language | English |
---|---|
Publication date | 4 Sep 2018 |
Number of pages | 20 |
Publication status | Published - 4 Sep 2018 |
Bibliographical note
Pre-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018
ID: 83355260