We are familiar with the notion of types as classifying what a program component does and permissible use of the component. A type system will tell us that a method call must have arguments of particular types and guarantee that it will return a value of a particular type.

This paper is a survey of work that goes beyond this, into type systems that classify in more detail possible interactions between program components. This is of particular relevance in concurrent computation where we might want to know not just the type of a single message that one component might send to another, but a pattern of interaction involving the interchange of several messages between two components. An example used throughout the paper to illustrate this is the pattern of interaction between a client and an ATM. One possible type of interaction is:

meaning the client first sends a request to be authorized to use the machine; then a request for the current balance, which is returned; then a request to withdraw, followed by the amount to be withdrawn, which is either dispensed or notice is given that it would result in an overdraft; and then the interaction is concluded. The paper gives a good introduction to the general principles and variations of this sort of typing, with a comprehensive set of references to the many recent papers published in this area.