Session subtyping and multiparty compatibility using circular sequents

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

11 Citations (Scopus)
6 Downloads (Pure)

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.

Original languageEnglish
Title of host publication31st International Conference on Concurrency Theory, CONCUR 2020
EditorsIgor Konnov, Laura Kovacs
Pages12.1-12.22
Number of pages22
Volume171
ISBN (Electronic)9783959771603
DOIs
Publication statusPublished - 26 Aug 2020
Event31st International Conference on Concurrency Theory, CONCUR 2020 - Virtual, Vienna, Austria
Duration: 1 Sept 20204 Sept 2020

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume171
ISSN (Print)1868-8969

Conference

Conference31st International Conference on Concurrency Theory, CONCUR 2020
Country/TerritoryAustria
CityVirtual, Vienna
Period1/09/204/09/20

Keywords

  • compatibility
  • deadlock freedom
  • linear logic
  • session types
  • subtyping
  • theory of computation
  • compatible process
  • non-commutative logic
  • structural proof theory
  • multi-party sessions

Fingerprint

Dive into the research topics of 'Session subtyping and multiparty compatibility using circular sequents'. Together they form a unique fingerprint.

Cite this