Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types

TL;DR

This paper demonstrates how generalized inference systems with corules can effectively characterize combined safety and liveness properties in binary session types, simplifying proofs and providing insights into protocol behaviors.

Contribution

It introduces the use of corules within generalized inference systems to characterize complex combined properties of session types, including fair termination and compliance.

Findings

Simpler characterizations compared to previous methods

Corules provide insight into liveness properties

Bounded coinduction ensures completeness

Abstract

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.