A sound algorithm for asynchronous session subtyping
File(s)LIPIcs-CONCUR-2019-38.pdf (586.76 KB)
Published version
Author(s)
Bravetti, Mario
Carbone, Marco
Lange, Julien
Yoshida, Nobuko
Zavattaro, Gianluigi
Type
Conference Paper
Abstract
Session types, types for structuring communication between endpoints in distributed systems, arerecently being integrated into mainstream programming languages. In practice, a very importantnotion for dealing with such types is that of subtyping, since it allows for typing larger classes ofsystem, where a program has not precisely the expected behavior but a similar one. Unfortunately,recent work has shown that subtyping for session types in an asynchronous setting is undecidable.To cope with this negative result, the only approaches we are aware of either restrict the syntaxof session types or limit communication (by considering forms of bounded asynchrony). Bothapproaches are too restrictive in practice, hence we proceed differently by presenting an algorithm forchecking subtyping which is sound, but not complete (in some cases it terminates without returninga decisive verdict). The algorithm is based on a tree representation of the coinductive definition ofasynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence offinite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements ouralgorithm and we apply it to many examples that cannot be managed with the previous approaches.
Date Issued
2019-08-26
Date Acceptance
2019-06-14
Citation
LIPIcs : Leibniz International Proceedings in Informatics, 2019, 140 (38), pp.38:1-38:16
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Start Page
38:1
End Page
38:16
Journal / Book Title
LIPIcs : Leibniz International Proceedings in Informatics
Volume
140
Issue
38
Copyright Statement
©Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro;licensed under Creative Commons License CC-BY (https://creativecommons.org/licenses/by/3.0/)
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20131167
EP/K011715/1
EP/N027833/1
20103649
Source
30th International Conference on Concurrency Theory
Publication Status
Published
Start Date
2019-08-26
Finish Date
2019-08-31
Coverage Spatial
Amsterdam, The Netherlands