Psi-calculi: Mobile Processes, Nominal Data, and Logic

A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations. Other proposed extensions of the pi-calculus can be formulated as psi-calculi; examples include the applied picalculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and a predicate logic for assertions. Our labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. We establish minimal requirements on the nominal data and logic in order to prove general algebraic propertie...

• Type: Conference
• Year: 2009
• Where: LICS
• Authors: Jesper Bengtson, Magnus Johansson, Joachim Parrow, Björn Victor
• Keywords: Computer Science, Labelled Operational Semantics, LICS 2009, Nominal Data, Pi-calculus