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.

A Sound Algorithm for Asynchronous Session Subtyping / Bravetti, Mario and Carbone, Marco and Lange, Julien and Yoshida, Nobuko and Zavattaro, Gianluigi. - ELETTRONICO. - (2019), pp. 38.1-38.16. (Intervento presentato al convegno CONCUR 2019 - Concurrency Theory, 30th International Conference tenutosi a Amsterdam, The Netherlands nel August 26-31, 2019) [10.4230/LIPIcs.CONCUR.2019.38].

A Sound Algorithm for Asynchronous Session Subtyping

Bravetti, Mario;Zavattaro, Gianluigi
2019

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.
2019
CONCUR 2019 - Concurrency Theory, 30th International Conference. Amsterdam, The Netherlands, August 26-31, 2019. Proceedings
1
16
A Sound Algorithm for Asynchronous Session Subtyping / Bravetti, Mario and Carbone, Marco and Lange, Julien and Yoshida, Nobuko and Zavattaro, Gianluigi. - ELETTRONICO. - (2019), pp. 38.1-38.16. (Intervento presentato al convegno CONCUR 2019 - Concurrency Theory, 30th International Conference tenutosi a Amsterdam, The Netherlands nel August 26-31, 2019) [10.4230/LIPIcs.CONCUR.2019.38].
Bravetti, Mario and Carbone, Marco and Lange, Julien and Yoshida, Nobuko and Zavattaro, Gianluigi
File in questo prodotto:
File Dimensione Formato  
preview.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione (CCBY)
Dimensione 586.28 kB
Formato Adobe PDF
586.28 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/690920
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? ND
social impact