License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.12
URN: urn:nbn:de:0030-drops-128245
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12824/
Go to the corresponding LIPIcs Volume Portal

Horne, Ross

Session Subtyping and Multiparty Compatibility Using Circular Sequents

pdf-format:
LIPIcs-CONCUR-2020-12.pdf (0.7 MB)

Abstract

We present a structural proof theory for multi-party sessions, exploiting the expressive power of non-commutative logic which can capture explicitly the message sequence order in sessions. The approach in this work uses a more flexible form of subtyping than standard, for example, allowing a single thread to be substituted by multiple parallel threads which fulfil the role of the single thread. The resulting subtype system has the advantage that it can be used to capture compatibility in the multiparty setting (addressing limitations of pairwise duality). We establish standard results: that the type system is algorithmic, that multiparty compatible processes which are race free are also deadlock free, and that subtyping is sound with respect to the substitution principle. Interestingly, each of these results can be established using cut elimination. We remark that global types are optional in this approach to typing sessions; indeed we show that this theory can be presented independently of the concept of global session types, or even named participants.

BibTeX - Entry

@InProceedings{horne:LIPIcs:2020:12824,
  author =	{Ross Horne},
  title =	{{Session Subtyping and Multiparty Compatibility Using Circular Sequents}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{12:1--12:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Igor Konnov and Laura Kov{\'a}cs},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12824},
  URN =		{urn:nbn:de:0030-drops-128245},
  doi =		{10.4230/LIPIcs.CONCUR.2020.12},
  annote =	{Keywords: session types, subtyping, compatibility, linear logic, deadlock freedom}
}

Keywords: session types, subtyping, compatibility, linear logic, deadlock freedom
Collection: 31st International Conference on Concurrency Theory (CONCUR 2020)
Issue Date: 2020
Date of publication: 26.08.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI