The first application relates to the design of a programming model of distributed and mobile computation. Relying on a distributed version of the asynchonous pi-calculus, we show that a simple type system ensures `receptiveness', i.e., that any message will find an appropriate receiver. We will argue that this property can be obtained without loss of expressive power.
The second application relates to the modelling and verification of cryptographic protocols relying on a simplified pi-calculus equipped with a `cryptographic table'. The latter is a data structures representing relationships among names. Following classical approaches, we formulate the verification task as a reachability problem and prove its decidability assuming finite principals and bounds on the sorts of the messages synthesized by the attacker.
This talk is partially based on joint work with G. Boudol, C. Lhoussaine, and S. Prasad.