The pi calculus was defined by Milner, Parrow, and Walker as a "Calculus of Mobile Processes". It provides an underlying formal model for interactive systems that can change their configuration on the fly; this spans a large spectrum from mobile telephone networks to Java-like languages. The calculus aims to be a model for interactive behaviour as basic as the lambda calculus is for sequential computation. In fact, the lambda calculus can be modelled straightforwardly within the pi calculus, and thus sequential computation can be seen as a special case of interaction.

The pi calculus is very simple; in my talk, I shall presume no previous knowledge of it, but I shall not need to spend long in describing its primitive constructions. I shall focus on how it can be applied in particular, on how it admits a pleasant type system in which "type" can be understood to mean "pattern of interaction". In particular, I shall show how properties like "each mobile agent (e.g., ambulance, etc.) will never be connected to more than one transmitter station at a time" are statically checkable types.

If time allows, I shall briefly discuss the language PICT (for distributed interactive systems) based upon pi calculus by Pierce, and the application of pi calculus to model authentication protocols by Martin Abadi and Andrew Gordon.