Luca Ciccone ; Luca Padovani - Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types

lmcs:8335 - Logical Methods in Computer Science, August 31, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:27)2022
Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session TypesArticle

Authors: Luca Ciccone ; Luca Padovani

    Many properties of communication protocols combine safety and liveness aspects. Characterizing such combined properties by means of a single inference system is difficult because of the fundamentally different techniques (coinduction and induction, respectively) usually involved in defining and proving them. In this paper we show that Generalized Inference Systems allow us to obtain sound and complete characterizations of (at least some of) these combined inductive/coinductive properties of binary session types. In particular, we illustrate the role of corules in characterizing fair termination (the property of protocols that can always eventually terminate), fair compliance (the property of interactions that can always be extended to reach client satisfaction) and fair subtyping, a liveness-preserving refinement relation for session types. The characterizations we obtain are simpler compared to the previously available ones and corules provide insight on the liveness properties being ensured or preserved. Moreover, we can conveniently appeal to the bounded coinduction principle to prove the completeness of the provided characterizations.


    Volume: Volume 18, Issue 3
    Published on: August 31, 2022
    Accepted on: June 22, 2022
    Submitted on: August 4, 2021
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 2075 times.
    This article's PDF has been downloaded 505 times.