Next: Personnel and exchanges
Up: University of Cambridge
Previous: University of Cambridge
The research at Cambridge that is most relevant to CONFER 2 has been
focused on the dynamics of action calculi, on the structure of
higherorder 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 calculus is mobile in this sense, whilst many other calculi such
as CCS, the 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 calculus is more expressive than, say, CCS.

Gardner has introduced a typetheoretic description of action
calculi [GH97] which develops her previous work on a namefree
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 typetheoretic account
of higherorder action calculi corresponds to Moggi's commutative
computational 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 higherorder
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.
 Higherorder reflexive action calculi The first of
these examples required two previously separate enrichments of AC,
namely, the higherorder and the reflexive extensions (the latter in a
simplified form). The proof that an AC combining the two is
welldefined reduces to a proof of strong normalisation for the
higherorder betareduction 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 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 INRIASophiaAntipolis) 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 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 calculus has been introduced, in which the input and output
capabilities of channels may be either global or local. This allows
compiletime optimization where possible but retains the
expressiveness of channel communication. Subtyping allows all
communications to be invoked uniformly.
The distributed calculus used integrates location and
migration primitives from the Distributed Join Calculus with
asynchronous 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].
Next: Personnel and exchanges
Up: University of Cambridge
Previous: University of Cambridge
1/10/1998