Subtyping Context-Free Session Types

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 subt...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2023-09
Main Authors: Silva, Gil, Mordido, Andreia, Vasconcelos, Vasco T
Format: Article
Language:English
Subjects:
Algorithms
Context
Programming languages
Simulation
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422
DOI:10.48550/arxiv.2307.05661