Chapter 2 Executive summary
The CONFER-2 Working Group follows Basic Research Action CONFER. It is
a framework to keep together the CONFER community, and to provide 2
annual workshops.
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 1
:
- Foundational Models and Abstract Machines
- Calculi
- Logics for Concurrency and the l-calculus
- Programming Languages
In the second year of CONFER-2,
work has progressed well in many areas. Below is a short summary of
some of the results, grouped according to main areas. For further
details see the site reports in chapter 3.
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, jocaml 1.07 has been released by le
Fessant. It is an extension of the virtual machine of Objective Caml
(Ocaml), which allows full compatibility with Ocaml. jocaml is
much faster than the first implementation of the join-calculus, and
more expressible, since it allows to freely use communication channels
inside Caml or to send any Caml data-structure on a channel.
Pisa has introduced the language KLAIM (Kernel Language for
Agents Interaction and Mobility). KLAIM is an experimental
programming language, inspired by the Linda paradigm, where mobile
agents and their coordination strategies can be naturally programmed.
KLAIM provides direct support for expressing and enforcing
security policies that control access to resources and data. In
particular, the language uses types to protect resources and data and
to establish policies for access control.
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