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

In: Logical Methods in Computer Science, Vol. 17, No. 1, 04.03.2021, p. 1-35.

Research output: Contribution to journalArticlepeer-review

Published

Standard

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

In: Logical Methods in Computer Science, Vol. 17, No. 1, 04.03.2021, p. 1-35.

Research output: Contribution to journalArticlepeer-review

Harvard

Bravetti, M, Carbone, M, Lange, J, Yoshida, N & Zavattaro, G 2021, 'A Sound Algorithm for Asynchronous Session Subtyping and its Implementation', Logical Methods in Computer Science, vol. 17, no. 1, pp. 1-35. <https://lmcs.episciences.org/7238>

APA

Bravetti, M., Carbone, M., Lange, J., Yoshida, N., & Zavattaro, G. (2021). A Sound Algorithm for Asynchronous Session Subtyping and its Implementation. Logical Methods in Computer Science, 17(1), 1-35. https://lmcs.episciences.org/7238

Vancouver

Bravetti M, Carbone M, Lange J, Yoshida N, Zavattaro G. A Sound Algorithm for Asynchronous Session Subtyping and its Implementation. Logical Methods in Computer Science. 2021 Mar 4;17(1):1-35.

Author

Bravetti, Mario ; Carbone, Marco ; Lange, Julien ; Yoshida, Nobuko ; Zavattaro, Gianluigi. / A Sound Algorithm for Asynchronous Session Subtyping and its Implementation. In: Logical Methods in Computer Science. 2021 ; Vol. 17, No. 1. pp. 1-35.

BibTeX

@article{a55ea6806ef64d3c8103514d62ed487a,
title = "A Sound Algorithm for Asynchronous Session Subtyping and its Implementation",
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 behaviour 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. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.",
author = "Mario Bravetti and Marco Carbone and Julien Lange and Nobuko Yoshida and Gianluigi Zavattaro",
year = "2021",
month = mar,
day = "4",
language = "English",
volume = "17",
pages = "1--35",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "1",

}

RIS

TY - JOUR

T1 - A Sound Algorithm for Asynchronous Session Subtyping and its Implementation

AU - Bravetti, Mario

AU - Carbone, Marco

AU - Lange, Julien

AU - Yoshida, Nobuko

AU - Zavattaro, Gianluigi

PY - 2021/3/4

Y1 - 2021/3/4

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 behaviour 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. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.

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 behaviour 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. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.

M3 - Article

VL - 17

SP - 1

EP - 35

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

ER -