Fair Subtyping for Multi-Party Session Types

International audience We study a theory of session types in which we add a liveness property to the familiar safety one. In this setting, some subtype relations between session types that hold in other theories and that are commonly regarded as harmless become unsound. We present various equivalent...

Full description

Bibliographic Details
Main Author: Padovani, Luca
Other Authors: Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Wolfgang Meuter, Gruia-Catalin Roman, TC 6, WG 6.1
Format: Conference Object
Language:English
Published: HAL CCSD 2011
Subjects:
Subtyping
session types
liveness properties
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Iceland
Online Access:https://hal.archives-ouvertes.fr/hal-00546531
https://hal.archives-ouvertes.fr/hal-00546531v2/document
https://hal.archives-ouvertes.fr/hal-00546531v2/file/main.pdf
https://doi.org/10.1007/978-3-642-21464-6_9
Description
Summary:International audience We study a theory of session types in which we add a liveness property to the familiar safety one. In this setting, some subtype relations between session types that hold in other theories and that are commonly regarded as harmless become unsound. We present various equivalent definitions of the subtyping relation, we relate it with the standard ones, and we give algorithms for deciding it. Incidentally, we provide an original and remarkably simple coinductive characterization of the fair testing preorder for nondeterministic, sequential processes consisting of internal choices of outputs and external choices of inputs.

Similar Items