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.

Peter.Sewell@cl.cam.ac.uk