Multiparty Classical Choreographies

Marco Carbone; Luís Cruz-Filipe; Fabrizio Montesi; Agata Murawska

doi:10.1007/978-3-030-13838-7_4

Multiparty Classical Choreographies

Marco Carbone
, Luís Cruz-Filipe
, Fabrizio Montesi
, Agata Murawska

Programming Logic and Semantics

University of Southern Denmark

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Abstract

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.

Original language	English
Journal	Lecture Notes in Computer Science
Volume	11408
Pages (from-to)	59-76
Number of pages	18
DOIs	https://doi.org/10.1007/978-3-030-13838-7_4
Publication status	Published - 23 Feb 2019
Event	International Symposium on Logic-Based Program Synthesis and Transformation - Frankfurt, Germany Duration: 4 Sept 2018 → 6 Sept 2018 Conference number: 28 https://research.com/conference/lopstr-2018

Symposium

Symposium	International Symposium on Logic-Based Program Synthesis and Transformation
Number	28
Country/Territory	Germany
City	Frankfurt
Period	04/09/2018 → 06/09/2018
Internet address	https://research.com/conference/lopstr-2018

Keywords

Multiparty session types
Choreography languages
Linear logic
Hypersequents
Server invocation

Access to Document

10.1007/978-3-030-13838-7_4

Cite this

@inproceedings{b46bf0dcbbf243c8b8443d4dac486cae,

title = "Multiparty Classical Choreographies",

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

keywords = "Multiparty session types, Choreography languages, Linear logic, Hypersequents, Server invocation",

author = "Marco Carbone and Lu{\'i}s Cruz-Filipe and Fabrizio Montesi and Agata Murawska",

note = "28th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2018 ; Conference date: 04-09-2018 Through 06-09-2018; International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR ; Conference date: 04-09-2018 Through 06-09-2018",

year = "2019",

month = feb,

day = "23",

doi = "10.1007/978-3-030-13838-7\_4",

language = "English",

volume = "11408",

pages = "59--76",

journal = "Lecture Notes in Computer Science",

url = "https://research.com/conference/lopstr-2018",

}

TY - GEN

T1 - Multiparty Classical Choreographies

AU - Carbone, Marco

AU - Cruz-Filipe, Luís

AU - Montesi, Fabrizio

AU - Murawska, Agata

N1 - Conference code: 28

PY - 2019/2/23

Y1 - 2019/2/23

N2 - 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.

AB - 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.

KW - Multiparty session types

KW - Choreography languages

KW - Linear logic

KW - Hypersequents

KW - Server invocation

U2 - 10.1007/978-3-030-13838-7_4

DO - 10.1007/978-3-030-13838-7_4

M3 - Conference article

VL - 11408

SP - 59

EP - 76

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - International Symposium on Logic-Based Program Synthesis and Transformation

Y2 - 4 September 2018 through 6 September 2018

ER -

Multiparty Classical Choreographies

Abstract

Symposium

Keywords

Access to Document

Fingerprint

Cite this