Polymorphic Lambda Calculus with Context-Free Session Types

TL;DR

This paper introduces context-free session types in a polymorphic lambda calculus, enabling fully type-safe serialization of complex recursive data structures, and addresses associated theoretical challenges.

Contribution

It extends System F with linear and context-free session types, providing a formal foundation for recursive communication protocols with type safety.

Findings

Developed the language FreeST 2 with context-free session types

Proved type preservation and progress theorems

Addressed contractivity and decidability challenges

Abstract

Context-free session types provide a typing discipline for recursive structured communication protocols on bidirectional channels. They overcome the restriction of regular session type systems to tail recursive protocols. This extension enables us to implement serialisation and deserialisation of tree structures in a fully type-safe manner. We present the theory underlying the language FreeST 2, which features context-free session types in an extension of System F with linear types and a kind system to distinguish message types and channel types. The system presents some metatheoretical challenges, which we address, contractivity in the presence of polymorphism, a non-trivial equational theory on types, and decidability of type equivalence. We also establish standard results on type preservation, progress, and a characterisation of erroneous processes.