文章基本信息

标题：A Sound Algorithm for Asynchronous Session Subtyping and its Implementation
本地全文：下载
作者：Zavattaro, Gianluigi ; Yoshida, Nobuko ; Lange, Julien 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2021
卷号：17
期号：1
页码：1-35
语种：English
出版社：Technical University of Braunschweig
摘要：Session types, types for structuring communication between endpoints indistributed systems, are recently being integrated into mainstream programminglanguages. In practice, a very important notion for dealing with such types isthat of subtyping, since it allows for typing larger classes of system, where aprogram has not precisely the expected behaviour but a similar one.Unfortunately, recent work has shown that subtyping for session types in anasynchronous setting is undecidable. To cope with this negative result, theonly approaches we are aware of either restrict the syntax of session types orlimit communication (by considering forms of bounded asynchrony). Bothapproaches are too restrictive in practice, hence we proceed differently bypresenting an algorithm for checking subtyping which is sound, but not complete(in some cases it terminates without returning a decisive verdict). Thealgorithm is based on a tree representation of the coinductive definition ofasynchronous subtyping; this tree could be infinite, and the algorithm checksfor the presence of finite witnesses of infinite successful subtrees.Furthermore, we provide a tool that implements our algorithm. We use this toolto test our algorithm on many examples that cannot be managed with the previousapproaches, and to provide an empirical evaluation of the time and space costof the algorithm.
关键词：Computer Science - Programming Languages