System $F^\mu_\omega$ with Context-free Session Types

TL;DR

This paper introduces an advanced type system extending polymorphic lambda calculus with context-free session types, providing decidability results and a concurrent language with guaranteed safety properties.

Contribution

It develops a novel type system with context-free session types, establishes decidability of type equivalence, and demonstrates a safe, expressive concurrent language.

Findings

Type equivalence is decidable for a significant fragment.

Type translation into automata models aids in decidability analysis.

The language guarantees preservation and absence of runtime errors.

Abstract

We study increasingly expressive type systems, from $F^\mu$ -- an extension of the polymorphic lambda calculus with equirecursive types -- to $F^{\mu;}_\omega$ -- the higher-order polymorphic lambda calculus with equirecursive types and context-free session types. Type equivalence is given by a standard bisimulation defined over a novel labelled transition system for types. Our system subsumes the contractive fragment of $F^\mu_\omega$ as studied in the literature. Decidability results for type equivalence of the various type languages are obtained from the translation of types into objects of an appropriate computational model: finite-state automata, simple grammars and deterministic pushdown automata. We show that type equivalence is decidable for a significant fragment of the type language. We further propose a message-passing, concurrent functional language equipped with the expressive type language and show that it enjoys preservation and absence of runtime errors for typable processes.