Declarative interpretations of session-based concurrency

Session-based concurrency is a type-based approach to the analysis 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 concurrency. We propose two interpretations of session π-calculus processes as declarative processes in linear concurrent constraint programming (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 π-calculus mobility. Categories and Subject Descriptors D.3.1 [Programming languages]: Formal Definitions and Theory; F.3.2 [Logics and meanings of programs]: Semantics of Programming Languages–Process models Keywords concurrency, ...

• Type: Journal
• Year: 2015
• Where: PPDP
• Authors: Mauricio Cano, Camilo Rueda, Hugo A. López, Jorge A. Pérez
• Keywords: PPDP 2015, Programming Languages