TY - JOUR
T1 - Corecursion and non-divergence in session-typed processes
AU - Toninho, Bernardo
AU - Caires, Luis
AU - Pfenning, Frank
PY - 2014/1/1
Y1 - 2014/1/1
N2 - Session types are widely accepted as an expressive discipline for structuring communications in concurrent and distributed systems. In order to express infinitely unbounded 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 π-calculus with general (co)recursion, while still allowing interesting infinite behaviors to be definable. Our approach builds on a Curry-Howard correspondence 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 compositionally non-divergent, that is, that no well-typed composition of processes, including those dynamically assembled via name passing, can result in divergent behavior.
AB - Session types are widely accepted as an expressive discipline for structuring communications in concurrent and distributed systems. In order to express infinitely unbounded 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 π-calculus with general (co)recursion, while still allowing interesting infinite behaviors to be definable. Our approach builds on a Curry-Howard correspondence 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 compositionally non-divergent, that is, that no well-typed composition of processes, including those dynamically assembled via name passing, can result in divergent behavior.
KW - Logical Predicate
KW - Linear Logic
KW - Session Type
KW - Divergent Behavior
KW - Process Calculus
UR - http://www.scopus.com/inward/record.url?scp=84996598696&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-45917-1_11
DO - 10.1007/978-3-662-45917-1_11
M3 - Article
AN - SCOPUS:84996598696
SN - 0302-9743
VL - 8902
SP - 159
EP - 175
JO - Lecture Notes in Computer Science (LNCS)
JF - Lecture Notes in Computer Science (LNCS)
ER -