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

Syddansk Universitet

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Konferenceartikel › Forskning › 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.

Originalsprog	Engelsk
Tidsskrift	Lecture Notes in Computer Science
Vol/bind	11408
Sider (fra-til)	59-76
Antal sider	18
DOI	https://doi.org/10.1007/978-3-030-13838-7_4
Status	Udgivet - 23 feb. 2019
Begivenhed	International Symposium on Logic-Based Program Synthesis and Transformation - Frankfurt, Tyskland Varighed: 4 sep. 2018 → 6 sep. 2018 Konferencens nummer: 28 https://research.com/conference/lopstr-2018

Symposium

Symposium	International Symposium on Logic-Based Program Synthesis and Transformation
Nummer	28
Land/Område	Tyskland
By	Frankfurt
Periode	04/09/2018 → 06/09/2018
Internetadresse	https://research.com/conference/lopstr-2018

Adgang til dokumentet

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

Citationsformater

@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

Adgang til dokumentet

Fingeraftryk

Citationsformater