Bravetti, Mario, Carbone, Marco, Lange, Julien, Yoshida, Nobuko, Zavattaro, Gianluigi (2019) A Sound Algorithm for Asynchronous Session Subtyping. In: Fokkink, Wan and van Glabbeek, Rob, eds. Leibniz International Proceedings in Informatics. 140. LIPICS ISBN 978-3-95977-121-4. (doi:10.4230/LIPIcs.CONCUR.2019.34) (KAR id:75503)
PDF
Author's Accepted Manuscript
Language: English
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
Download (738kB)
Preview
|
Preview |
This file may not be suitable for users of assistive technology.
Request an accessible format
|
|
Official URL http://dx.doi.org/10.4230/LIPIcs.CONCUR.2019.34 |
Abstract
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of
of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm and we apply it to many examples that cannot be managed with the previous approaches.
Item Type: | Conference or workshop item (Paper) |
---|---|
DOI/Identification number: | 10.4230/LIPIcs.CONCUR.2019.34 |
Uncontrolled keywords: | Session types, Concurrency, Subtyping, Algorithm. |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Julien Lange |
Date Deposited: | 23 Jul 2019 09:39 UTC |
Last Modified: | 16 Feb 2021 14:06 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/75503 (The current URI for this page, for reference purposes) |
Lange, Julien: | ![]() |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):