Characteristic Formulae for Session Types (extended version)

TL;DR

This paper introduces an algorithm that generates modal mu-calculus formulas to effectively determine subtype relations in session types, enabling the use of model checkers for efficient safety verification.

Contribution

It presents a novel characteristic formulae approach and an algorithm for subtyping checks in session types, enhancing efficiency and integration with model checking.

Findings

Algorithm accurately characterizes subtypes and supertypes

Implementation compares favorably with classical subtyping algorithms

Enables safety verification via model checkers

Abstract

Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the problem. Our core contribution is an algorithm to generate a modal mu-calculus formula that characterises all the supertypes (or subtypes) of a given type. Subtyping checks can then be off-loaded to model checkers, thus incidentally yielding an efficient algorithm to check safety of session types, soundly and completely. We have implemented our theory and compared its cost with other classical subtyping algorithms.