Multiparty Classical Choreographies

Marco Carbone, Luís Cruz-Filipe, Fabrizio Montesi, Agata Murawska [2018].
In proceedings of LOPSTR 2018, pp. 59-76.

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.
Additional notes
Cite (BibTeX)
Click to expand
  author       = {Marco Carbone and
                  Lu{\'{\i}}s Cruz{-}Filipe and
                  Fabrizio Montesi and
                  Agata Murawska},
  editor       = {Fred Mesnard and
                  Peter J. Stuckey},
  title        = {Multiparty Classical Choreographies},
  booktitle    = {Logic-Based Program Synthesis and Transformation - 28th International
                  Symposium, {LOPSTR} 2018, Frankfurt/Main, Germany, September 4-6,
                  2018, Revised Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {11408},
  pages        = {59--76},
  publisher    = {Springer},
  year         = {2018},
  url          = {\_4},
  doi          = {10.1007/978-3-030-13838-7\_4},
  timestamp    = {Wed, 25 Sep 2019 18:04:29 +0200},
  biburl       = {},
  bibsource    = {dblp computer science bibliography,}

A PDF is available (possibly a preprint):

Download PDF