# 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.