Subtyping Context-Free Session Types

TL;DR

This paper introduces a new subtyping approach for context-free session types using an innovative observational preorder called $\\ ext{XYZW}$-simulation, enabling more expressive communication protocol specifications with a sound subtyping algorithm.

Contribution

It presents a novel $\\text{XYZW}$-simulation-based subtyping method for context-free session types, extending prior simulation concepts and providing a practical, sound algorithm.

Findings

The subtyping algorithm is proven sound.

Empirical evaluation demonstrates practical applicability.

The approach generalizes existing simulation relations.

Abstract

Context-free session types describe structured patterns of communication on heterogeneously-typed channels, allowing the specification of protocols unconstrained by tail recursion. The enhanced expressive power provided by non-regular recursion comes, however, at the cost of the decidability of subtyping, even if equivalence is still decidable. We present an approach to subtyping context-free session types based on a novel kind of observational preorder we call $\mathcal{XYZW}$-simulation, which generalizes $\mathcal{XY}$-simulation (also known as covariant-contravariant simulation) and therefore also bisimulation and plain simulation. We further propose a subtyping algorithm that we prove to be sound, and present an empirical evaluation in the context of a compiler for a programming language. Due to the general nature of the simulation relation upon which it is built, this algorithm may also find applications in other domains.