The overall objective of the CONFER-2 action is similar to the one of CONFER and to create both the theoretical foundations and the technology for combining the expressive power of the functional and the concurrent computational models. The action is organised around four main areas

- Foundational Models and Abstract Machines
- Calculi
- Logics for Concurrency and the l-calculus
- Programming Languages

In the area of Foundational Models and Abstract Machines progress has been made in three main directions.

Firstly the categorical understanding of models of process calculi has been furthered by recent work by Gian Luca Cattani on presheaf categories as denotational models of concurrent process calculi. Also work by Gardner and Wischik on the graphical understanding of the p-calculus takes advantage of categorical models. A symmetric version of action calculi is giving a simpler and more natural way of representing the p-calculus graphically.

Secondly the work on game semantics is maturing. Recently Abramsky, Honda and McCusker used game semantics to give the first fully abstract model for a language with higher-order functions and general reference types---a substantial fragment of ``real'' languages such as SML and SCHEME. Also a first bridge between dynamic semantics and static semantics of functional languages has been given using game semantics.

Thirdly research has continued on developing the mathematical foundations of mobile systems based on the tile logic. The natural targets of the tile approach are models of mobile systems which are compositional in both space and time.

In the area of Calculi several studies of objects have been undertaken. A class-based calculus of concurrent objects has been obtained by Fournet, Maranget, Laneve and Rémy from the join-calculus by introducing primitive record structure. Also Kleist and Sangiorgi have given an interpretation of Abadi and Cardelli's first-order Imperative Object Calculus into a typed p-calculus, and Silvano Dal-Zilio has used the modelisation of Abadi and Cardelli objects in the blue calculus extended with a very simple system of localities.

Also in the area of Calculi there has recently been a growing interest in asynchronous languages and process calculi, where message emission is non-blocking. An important reference for this class of languages is the asynchronous pi-calculus. Castellani and Hennessy have studied testing semantics for asynchronous process calculi and their descriptive power has now been largely demonstrated. Massimo Merro has shown that the asynchronous p-calculus is powerful enough to encode asynchronous variants of the Chi, Update, and Fusion calculi which are modifications of the p-calculus in which communications have a more global scope. Victor has developed a broad foundational theory of the fusion calculus, both labelled and unlabelled operational semantics, and treated strong and weak bisimulation equivalences for both semantics in some detail.

Milner and Sawle are defining and investigating the polynomial pi-calculus, which may be described as the pi-calculus extended by multiway communication. Although not so easy to implement, this notion is quite attractive because it is extremely powerful, formally speaking. For example, guarded summation is derivable, up to strong (not weak) equivalence; the calculus also appears to have some advantage in expressing security protocols.

Considerable progress has been made towards an understanding of operational congruences for arbitrary calculi defined by reduction semantics by Leifer and Sewell. Leifer gave bisimulation congruence results for two sub-classes of action calculi, resting on algebraic results about action calculus context decompositions. Three simple classes were considered by Sewell, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding.

In the area of Logics for Concurrency and the l-calculus Klop and Bethke have worked on ``origin tracking'', both in the framework of first-order term rewriting and l-calculus. For first-order rewriting using this technique a proof was given of the theorem of Huet and Lévy on normalization of needed reductions. This technique is in the literature also called ``dynamic dependence tracking'' and is used for applications such as program slicing and error recovery. For l-calculus a corresponding notion of origin tracking using Lévy's labeled l- calculus was formulated and used to give a new proof of the classical Genericity Lemma in l-calculus.

In the area of Programming Languages Bologna has proceeded in the development of their implementation of Lamping's graph reduction algorithm for optimal reduction of functional languages and they have completed a new ``light'' version, essentially inspired by Girard's Light Linear Logic. Gardner and Norrish have experimented with the design and construction of specification tools for action graphs, which allow the user to naturally move between the syntactic and graphical presentations. Work on extending the implementation to reflexive action calculi is underway (in a student project). This is a non-trivial extension, which we hope will lead to a simpler implementation. Sewell, Unyapoth and Wojciechowski, in collaboration with Pierce, are studying the design, semantic definition and implementation of location-independent communication primitives for mobile agents. They have proposed two simple calculi of agents that can migrate between sites and can interact by both location dependent and location independent message passing. Work on an implementation, and on correctness proofs of the distributed algorithms involved, is ongoing.

CNET has investigated some aspects of low-level security in distributed programming languages, such as protecting hosts against potentially hostile mobile code in open environments. ICL has worked on transferring ideas from the Facile system to the Java world via the mlj (ML to Java Virtual Machine code) compiler from Persimmon Research. Interfaces for the Facile concurrency primitives have been implemented. ICL is currently looking into how various packages for Mobile Agents in Java can be used to implement (some of) the constructs for distributed computing from Facile. There are now two implementations of the join-calculus. Version 1.03 has been released in 1997 by Fournet and Maranget. This prototype includes a distributed implementation of the join-calculus. In June 1998,

As seen from the site reports in chapter 3, crossfertilisation of ideas among fellow researchers in the working group continues to be very lively. As in previous years it is evident that related work done at other sites in the consortium is referenced often and also very often used as the basis for development of new results. It is no surprise that a number of these results have been achieved in collaboration between sites, enabled through site visits for shorter or longer periods. Leading researchers outside the consortium have also been involved in fruitful collaborations.

During Year 2 of CONFER-2 two workshops have been held.

The working group has produced a large number (about 70) of reports and several of these have been published at conferences, international workshops and journals. Many of theses works are accessible at URL

http://www.cs.auc.dk/mobility/

where a Web page on Mobility is maintained by Uwe Nestmann, who moved in September 1997 from INRIA Rocquencourt to Aalborg.

Several Ph.D.'s are in preparation in the action, and several have been defended.

This report can be accessed on the World Wide Web at:

http://para.inria.fr/confer/

- 1
- see Periodic Progress Reports of CONFER for more explanations