Taming mobile processes using types

We discuss some examples of the use of types for taming the behavior of concurrent systems, in particular systems of mobile processes. By "taming" we mean that we use types to enforce expected - and desirable - properties of systems. These properties would not hold without types. The examples we discuss are a printer with mobile ownership, a Boolean package implementation, and the termination property. In all these examples, the solutions based on types are only sketched. Details on the types themselves (the formal systems and their basic properties), and on the proof techniques based on types with which the equalities in the examples are proved can be found following the reference pointers, especially the work of Sangiorgi and Walker (2001) and Sangiorgi (2001). The examples are presented in the /spl pi/-calculus described by Milner (1992), a paradigmatical process calculus for message-passing concurrency.