Corecursion in Session-Typed Processes

Abstract—Session types are widely accepted as a useful expres-sive discipline for structuring communications in concurrent and distributed systems. In order to express infinitely unbounded sessions, as required to model the behaviour of realistic dis-tributed systems, session typed languages often introduce general recursion operators at both the program and the type level. Unfortunately, general recursion, in particular when combined with name passing and mobility, may easily introduce undesirable divergence, e.g., infinite unobservable reduction sequences. In this paper we address, by means of typing, the challenge of ensuring non-divergence in a session-typed pi-calculus with general (co)recursion, while still allowing interesting infinite behaviours to be definable, as necessary to model realistic open process networks and distributed systems. Our approach builds on a Curry-Howard correspondence between our type system and a standard system of linear logic extended with co-inductive types, for which our non-divergence property implies consistency. We prove type safety for our framework, implying protocol compliance and global progress of well-typed processes. Remark-ably, we also establish- through a logical relations argument-that well-typed processes are compositionally non-divergent, in the sense that no well-typed composition of processes, including compositions dynamically assembled through name passing, can result in divergent behaviour, a property of practical relevance. I