Declarative Interpretations of Session-Based Concurrency

Session-based concurrency is a type-based approach to the analy-sis of communication-intensive systems. Correct behavior in these systems may be specified in an operational or declarative style: the former defines how interactions are structured; the latter defines governing conditions. In this paper, we investigate the relationship between operational and declarative models of session-based con-currency. We propose two interpretations of session pi-calculus pro-cesses as declarative processes in linear concurrent constraint pro-gramming (lcc). They offer a basis on which both operational and declarative requirements can be specified and reasoned about. By coupling our interpretations with a type system for lcc, we obtain robust declarative encodings of pi-calculus mobility