Corecursion in session-typed processes

Abstract. Session types are widely accepted as an expressive discipline for structuring communications in concurrent and distributed systems. In order to express infinitely un-bounded sessions, session typed languages often include general recursion which may 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. Our approach builds on a Curry-Howard correspon-dence between our type system and 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. We also establish, using a logical relation argument, that well-typed processes are com-positionally non-divergent, that is, that no well-typed composition of processes, includ-ing those dynamically assembled via name passing, can result in divergent behaviour.