Document Open Access Logo

A Sound Algorithm for Asynchronous Session Subtyping

Authors Mario Bravetti , Marco Carbone , Julien Lange , Nobuko Yoshida , Gianluigi Zavattaro



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.38.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Mario Bravetti
  • University of Bologna, Italy
  • INRIA FoCUS Team
Marco Carbone
  • IT University of Copenhagen, Denmark
Julien Lange
  • University of Kent, UK
Nobuko Yoshida
  • Imperial College London, UK
Gianluigi Zavattaro
  • University of Bologna, Italy
  • INRIA FoCUS Team

Cite AsGet BibTex

Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A Sound Algorithm for Asynchronous Session Subtyping. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 38:1-38:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.38

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • Session types
  • Concurrency
  • Subtyping
  • Algorithm

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail