Typed psi-calculi

Hans Huttel, University of Aalborg, Denmark

There are by now several process calculi that extend the pi-calculus with more general notions of messages. Bengtson et al. have introduced psi-calculi as a generalization of these many variants, and it has been shown that many existing process calculi can be captured as instances of this general framework.

We here describe a simple type system for psi-calculi. The type system satisfies a subject reduction property and satisfies a general notion of channel safety. A number of existing type systems are easily shown to be instances of our system, and other, new type systems can also be obtained by instantiation. In particular, we instantiate the type system to obtain a first type system for the calculus of explicit fusions by Wischik and Gardner, another for the distributed pi-calculus of Hennessy and Riely and finally show how existing type systems for secrecy and authenticity in the spi calculus can be represented and how the proofs of their safety is facilitated by the general properties of our type system.