Subtyping context-free session types

Session types are a type discipline for concurrent programming. They allow programmers to describe and enforce structured patterns of communication between processes on heterogeneous, bidirectional channels. Equipped with a sequential composition operator, context-free session types enjoy greater expressive power when compared to their traditional counterparts, which are limited to the specification of regular communication patterns. The introduction of subtyping allows programmers to draw on this enhanced expressive power to describe even richer behaviors while avoiding code duplication. In this work, we present the first dedicated study of subtyping for context-free session types, which has until now been only briefly considered and, somewhat discouragingly, found undecidable. Despite this unfortunate result, we define a rich notion of subtyping for context-free session types in a functional setting, and present two distint approaches to its formalization: one based on inference rules, the other based on a labelled transition system. For the latter, we introduce XYZW -simulations, a novel family of simulation relations that generalize both XY -simulations and polar simulations. We further propose a semi-algorithm for the problem, prove it to be sound, and evaluate it empirically in the context of a programming language compiler.

Authors

• Gil Silva
• Andreia Mordido
• Vasco T. Vasconcelos

Keywords

• Context-free session types
• Subtyping
• Simulation relations
• Non-regular recursion
• Simple grammars