Session subtyping and multiparty compatibility using circular sequents

Horne, Ross; Konnov, Igor and Kovacs, Laura, eds. (2020) Session subtyping and multiparty compatibility using circular sequents. In: 31st International Conference on Concurrency Theory, CONCUR 2020. Leibniz International Proceedings in Informatics, LIPIcs, 171 . Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, AUT, 12.1-12.22. ISBN 9783959771603 (https://doi.org/10.4230/LIPIcs.CONCUR.2020.12)

[thumbnail of Horne-CONCUR2020-Session-subtyping-multiparty-compatibility-using-circular-sequents]
Preview
 Text. Filename: Horne-CONCUR2020-Session-subtyping-multiparty-compatibility-using-circular-sequents.pdf
Final Published Version
License: Creative Commons Attribution 3.0 logo
Download (777kB)| Preview

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.

CORE (COnnecting REpositories)