ITU

A Sound Algorithm for Asynchronous Session Subtyping

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Standard

A Sound Algorithm for Asynchronous Session Subtyping. / Bravetti, Mario; Carbone, Marco; Lange, Julien; Yoshida, Nobuko; Zavattaro, Gianluigi.

In: Leibniz International Proceedings in Informatics, Vol. 140, 2019, p. 34:1–34:16.

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bravetti, Mario ; Carbone, Marco ; Lange, Julien ; Yoshida, Nobuko ; Zavattaro, Gianluigi. / A Sound Algorithm for Asynchronous Session Subtyping. In: Leibniz International Proceedings in Informatics. 2019 ; Vol. 140. pp. 34:1–34:16.

Bibtex

@inproceedings{959edafaa77e414db6938f855016cfee,
title = "A Sound Algorithm for Asynchronous Session Subtyping",
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 system, 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 syntax 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.",
author = "Mario Bravetti and Marco Carbone and Julien Lange and Nobuko Yoshida and Gianluigi Zavattaro",
year = "2019",
doi = "10.4230/LIPIcs.CONCUR.2019.34",
language = "English",
volume = "140",
pages = "34:1–34:16",
journal = "Leibniz International Proceedings in Informatics",
issn = "1868-8969",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH",
note = "30th International Conference on Concurrency Theory, CONCUR 2019 ; Conference date: 28-08-2019",

}

RIS

TY - GEN

T1 - A Sound Algorithm for Asynchronous Session Subtyping

AU - Bravetti, Mario

AU - Carbone, Marco

AU - Lange, Julien

AU - Yoshida, Nobuko

AU - Zavattaro, Gianluigi

PY - 2019

Y1 - 2019

N2 - 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 system, 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 syntax 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.

AB - 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 system, 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 syntax 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.

U2 - 10.4230/LIPIcs.CONCUR.2019.34

DO - 10.4230/LIPIcs.CONCUR.2019.34

M3 - Conference article

VL - 140

SP - 34:1–34:16

JO - Leibniz International Proceedings in Informatics

JF - Leibniz International Proceedings in Informatics

SN - 1868-8969

T2 - 30th International Conference on Concurrency Theory

Y2 - 28 August 2019

ER -

ID: 84744122