
The first application relates to the design of a programming model of distributed and mobile computation. Relying on a distributed version of the asynchonous picalculus, 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 picalculus 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.
© Björn Victor Last modified: Wed, 28Jul1999 13:07 MEST 