Research directions

The research at Cambridge that is most relevant to CONFER 2 has been focused on the dynamics of action calculi, on the structure of higher-order and reflexive action calculi, and on the foundations of concurrent and distributed programming languages.

Action Calculi

• Labelled transition systems and bisimulation congruences The semantics of a process calculus, several of which have been introduced during CONFER, can often be most intuitively given as a reduction relation, defined by a structural congruence and reduction axioms. The action calculus framework embraces a rather wide class of such definitions. A central problem is then that of deriving, from such a definition of reduction, a labelled transition semantics for which bisimulation is a satisfactory congruence. Considerable progress has been made, e.g. by Jensen [Jen98] for a form of graph rewriting approximating to a graphical presentation of action calculi, and by Sewell for special cases of term rewriting. Work on more general cases is being undertaken by Gardner, Jensen, Leifer, Milner and Sewell.
• Expressiveness A uniform framework for the operational semantics of calculi allows comparisons of expressiveness to be made. Using natural homomorphisms between control structures (the models of action calculi), it is possible to characterise important properties of calculi such as mobility of channels. Leifer has shown that the $\pi$-calculus is mobile in this sense, whilst many other calculi such as CCS, the $\lambda$-calculus, and Petri nets, are not. This work, extending the work of Mifsud at Edinburgh, gives a precise meaning to the intuitive sense in which the $\pi$-calculus is more expressive than, say, CCS.
• Gardner has introduced a type-theoretic description of action calculi [GH97] which develops her previous work on a name-free account of action calculi and gives a logical interpretation based on the general binding operators studied by Aczel. With her Ph.D student Hasegawa, at Edinburgh, she has shown that the type-theoretic account of higher-order action calculi corresponds to Moggi's commutative computational $\lambda$-calculus. With Gordon Plotkin and Andrew Barber, also at Edinburgh, they have introduced a further extension of action calculi, called the linear action calculi [BGHP97]. Linear action calculi extend the higher-order case, and the associated type theory corresponds to the linear type theories studied by Barber and Nick Benton of Cambridge. The conservative extension results follow from looking at the corresponding categorical models.
• Examples Several example action calculi have been considered, including a functional programming language with mutable store and exceptions, the ambient calculus of Abadi and Cardelli, and distributed process calculi.
• Higher-order reflexive action calculi The first of these examples required two previously separate enrichments of AC, namely, the higher-order and the reflexive extensions (the latter in a simplified form). The proof that an AC combining the two is well-defined reduces to a proof of strong normalisation for the higher-order beta-reduction of the molecular forms corresponding to this enriched AC. Leifer completed this proof and, in the process of doing so, developed several new techniques for handling molecular forms, including the formalisation of manipulations involving reflexive substitutions.

Concurrent and distributed programming languages Our work on programming languages builds on the PICT language, based on the $\pi$-calculus, of Pierce and Turner. PICT now has a stable public release; its design is described in [PT97]. Pierce, who has moved from Cambridge to Indiana, has continued to work on type inference and (with Sangiorgi of INRIA-Sophia-Antipolis) on bisimulation in the presence of polymorphism. We are collaborating on calculi for distribution.

• Observational semantics for concurrent programming languages Sewell has studied the semantics of PICT in [Sew97c], and has shown how the behaviour of implementations of the language relates precisely to the labelled transitions of the $\pi$-calculus. His results indicate that there is an essentially unique behavioural equivalence appropriate for PICT, from the large space of choices in the literature.
• Global/Local typing In the design of distributed programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. In [Sew97a] a static type system for a distributed $\pi$-calculus has been introduced, in which the input and output capabilities of channels may be either global or local. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. The distributed $\pi$-calculus used integrates location and migration primitives from the Distributed Join Calculus with asynchronous $\pi$ communication, with a simple reduction semantics that can be presented as an action calculus. Abstract machines for similar calculi have been considered by Unyapoth.
• Location Independence In [SWP97] we have begun to study in more detail the design, semantic definition and implementation of communication primitives by which mobile agents can interact. We have proposed a simple calculus of agents that can migrate between sites and can interact by both location dependent and location independent message passing. It has a precise reduction semantics. Implementations of the location independent primitives can be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. This allows the algorithms to be stated and understood precisely, a clean implementation strategy for prototype languages (such an encoding can be realized as one phase of a compiler), and reasoning. It also provides a setting in which multiple communication mechanisms can coexist gracefully.

  A prototype implementation, building on that of PICT, is ongoing, as is work on reasoning, in particular on correctness and robustness results.

Work has also been completed on the algebraic theory of processes [Sew97b] and on closed action calculi [Gar98].