We discuss some examples of the use of types for taming the behaviour 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 [SW01, Parts III and IV] and [San01].

The examples are presented in the π-calculus [MPW92], a paradigmatical process calculus for message-passing concurrency.