Iso-Recursive Multiparty Sessions and their Automated Verification

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 talk, 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.

(** Joint work with Nobuko Yoshida *