Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
Marco Giunti, Nobuko Yoshida
TL;DR
The paper addresses deadlock-freedom verification for generalised multiparty session types with iso-recursive types, proposing a computable compliance function built on a deterministic transition system for session environments and an environment-closure mechanism. It provides an OCaml implementation that handles non-determinism via exceptions and uses Why3 for automated verification, ensuring absence of mismatches and deadlocks. These contributions lead to decidable, self-contained type checking for GMST without relying on external model checkers, and they demonstrate practical feasibility through a certified implementation. The work also discusses future directions, including session delegation and asynchronous subtyping, to broaden the applicability of the framework.
Abstract
Most works on session types take an equi-recursive approach and do not distinguish among a recursive type and its unfolding. This becomes more important in recent type systems which do not require global types, also known as generalised multiparty session types (GMST). In GMST, in order to establish properties as deadlock-freedom, the environments which type processes are assumed to satisfy extensional properties holding in all infinite sequences. This is a problem because: (1) the mechanisation of GMST and equi-recursion in proof assistants is utterly complex and eventually requires co-induction; and (2) the implementation of GMST in type checkers relies on model checkers for environment verification, and thus the program analysis is not self-contained. In this paper, we overcome these limitations by providing an iso-recursive typing system that computes the behavioural properties of environments. The type system relies on a terminating function named compliance that computes all final redexes of an environment, and determines when these redexes do not contain mismatches or deadlocks: compliant environments cannot go wrong. The function is defined theoretically by introducing the novel notions of deterministic LTS of environments and of environment closure, and can be implemented in mainstream programming languages and compilers. We showcase an implementation in OCaml by using exception handling to tackle the inherent non-determinism of synchronisation of branching and selection types. We assess that the implementation provides the desired properties, namely absence of mismatches and of deadlocks in environments, by resorting to automated deductive verification performed in tools of the OCaml ecosystem relying on Why3.