The Pi-Calculus is a fundamental calculus for interactive computing defined in about 1990. Action structures were later introduced as a family of calculi (including the Pi-Calculus and many familiar models of computation such as the Lambda Calculus and Petri nets), with the aim of allowing such models to be compared and combined, and to develop their common theory.
This project has pursued two complementary threads: it has pushed the Pi-Calculus toward applications, and it has advanced the theory of action calculi (ACs). The participants have been Robin Milner, Benjamin Pierce, Peter Sewell, Philippa Gardner, Adriana Compagnoni and (as students) Ole Jensen, Jamey Leifer, Asis Unyapoth, Lucien Wischik and Pawel Wojciechowski.
The first thread started from Pict, a programming language for mobile computing, previously designed at Edinburgh. In the Cambridge project we have further developed Pict, e.g. by expanding the library and refining the type system, and used it in building more serious applications. A defining paper on the language was written, and one on its design. The language was taught to undergraduates. Several theoretical questions arising from the language definition were studied concerning: type systems which reflect properties of interactive behaviour; behavioural equivalence of programs; and abstract machines for implementing Pict. A major development of Pict was taken in the direction of distributed mobile computation, in collaboration with the Computer Laboratory's distributed systems group. The key advance has been in expressing the notion of location directly in the language, allowing proper distinction between local and non-local interactions, and paving the way for proper handling of localised failure (essential to good engineering). A combined practico-theoretical group has formed around this work in Cambridge, and the work is ongoing.
The second main thread of research has further explored action calculi. At the start, two main defining papers of action calculi and their interpretations were completed. Principal features of action calculi are their graphical presentation, the prominence given to the notion of naming (underlying concepts as diverse as program variables, pointers or references, and communication channels) and the new notion of name-abstraction. We also completed a combinatoric account of ACs, which highlights the important role played by name-abstraction. This project has advanced on many lines. First, we have explored the expressiveness of action calculi, finding that functional and imperative programming, Pi-Calculus, Petri nets and even modern calculi such as the Ambient Calculus of Cardelli and Gordon, all fit comfortably in the framework. With researchers at Edinburgh, we have given a propositions-as-types interpretation of ACs, which isolates what is distinctive about the AC framework. We have also found semantic methods of classifying individual action calculi according to various properties; thus the action calculus framework provides taxonomy. We have extended action calculi to admit higher-order notions and feedback (self-reference), and found that the theory extends smoothly. Finally, we have identified and partially solved a hard semantic problem, to define a notion of behavioural equivalence with tractable properties for a wide class of action calculi, which agrees with any specialized theory which exists for each individual calculus. We have a firm grasp of the problem - which is central to the whole theoretical development - and are tackling it intensively.
Summary The theory and practice of mobile interactive systems have been advanced in a satisfactory way; action calculi and Pi-Calculus are proving to have practical significance as well as tractable theory. Much further work is needed in both these directions.