Research directions

Value-passing processes

There were two publications in this area. In [Ra97a] an axiomatic characterisation of both late and early observational congruence for a class of fully parameterised processes is given. This result uses a new derivation rule which is an intuitive generalisation of unique fixpoint induction based on loop invariants for symbolic graphs. In the same paper it is shown that the new rule can actually be derived from existing formulations of unique fixpoint induction for value-passing calculi.

In [Ra97b] a first order modal mu-calculus is described which uses parameterised maximal fixpoints to describe safety and liveness properties of value-passing processes. A proof system for deciding if a process satisfies a formula is presented. Certain deduction rules of the system carry side conditions which leave auxiliary proof obligations of checking properties of the value language. Although the proof system is in general incomplete two completeness results are given for significant sub-logics.

Mathematical Models for concurrent languages

There are two streams of work here. The first, summarised in [Je97], gives a precise relationship between

• mixed data and control flow graphs , which are commonly used in software engineering as a semi-formal notation for describing and analysing algorithms
• and an abstract representation of formal semantics which uses partially traced Cartesian categories.

This document also contains some more speculative work on how closed structure (to represent higher-order functions) or two-category structure (to represent operational semantics) might be included in this graphical framework.

In [HaHen97e] traditional denotational techniques are used to give a denotational model of a subset of core Facile . Specifically this is applied typed call-by-value language which in addition to the usual types has an extra type for processes, which can exchange values along communication channels, a la CCS . The model is shown to be fully-abstract with respect to a version of may testing . It is notable that in order to achieve full-abstraction it is necessary to add to the language an operator which allows processes report the result of a computation.

Semantic theories for distributed processes

In [RieHen97a] location failure for distributed processes is studied in detail. A language is defined in which threads are run at distributed locations, and from this a semantic theory is developed using the basic notions of observer and experiment . Roughly, an observer interacts with a distributed process either by synchronizing with one of its threads or by halting one of its locations; two programs are equivalent if they present the same structure of observations, evolving over time. The main result of this work is to provide an alternative characterization of this observational equivalence which is suitable to automatic verification. This is done using a temporal logic to characterize the interdependence between synchronization events and failures.

In [RieHen97b] a more expressive language is presented, which includes agent migration, location failure and a rich system of capabilities used to tag communicated data. Intuitively, when the name, say, of a location is communicated, a set of capabilities for that location is communicated at the same time; these may include the capability to read data, to write data, to halt the location, to migrate to it, or to allocate fresh resources at it. We present a series of type systems for this language and show, through examples, that very expressive type systems are necessary in order to be able to type many important practical programs.