Previous Next Contents

Chapter 2:   Executive summary

The CONFER-2 Working Group is a framework to keep together the community of the previous Basic Research Action CONFER, and to provide two annual workshops. The objective of CONFER-2 is 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 organized around four main areas : In the area of Foundational Models and Abstract Machines, the research activity has progressed in three main areas.

Firstly a book by Asperti and Guerrini has been published at Cambride University Press. It summarizes the research on Optimal Reductions in the lambda calculus. This area has been very active in the last decade, especially inside our Working Group (see previous Progress Reports of CONFER and CONFER-2). In the same spirit, the study of origin tracking in the lambda calculus has been pursued by Klop at CWI.

Secondly, a result on the finiteness of the normalization cone in the lambda-sigma calculus has been published by Melliès on leave from University of Edinburgh to ENS. In the same spirit, Bruni, Gadduci, and Montanari have studied the connection between three reduction systems: rewriting logic (Meseguer), action calculi (Milner), and tile logic (Montanari). Both approaches are based on category theory.

Thirdly, the work on Action Calculi is still strongly developed at Cambridge. Action Calculi form an abstract model for calculi with bound variables and guards (preventing from computing below them). Leifer investigates general methods for deriving labeled transition systems from reduction rules in a way initiated by Milner and Sewell. Indeed labeled transition systems provide an intensional semantics describing the interactions of processes on contexts, and it would be useful to automatically derive bisimulations as congruences from the extensional semantics given in terms of reduction rules and observational equivalences. A correspondence between action calculus and the synchronous pi-calculus has been also studied by Gardner.
In the area of Calculi, progress has been made mainly in four directions.

Security, which is a major issue for distributed languages with mobile primitives, has been studied in various forms at different sites inside CONFER-2. Secure encapsulation is proposed by Sewell and Vitek as a way of assembling concurrent, software systems with untrusted or partially untrusted parts. Principals have been added to the join calculus by Abadi, Fournet and Gonthier. It allows formal statements about authentication and secrecy, which may be proved with standard proof techniques of process calculi. Another proof technique has been developed by Amadio and Prasad for the verification of secrecy and authentication with symmetric shared keys. Hennessy and Yoshida consider types as a way of expressing locality in the pi-calculus. Finally, a dependency calculus is studied by Conchon and Pottier for descriptions of static interference properties using data flow techniques.

The theory of asynchronous bisimulations equivalences has been intensively considered. A tutorial on asynchronous calculi has been published by Sangiorgi. The work on the connection between the synchronous and asynchronous pi-calculi is pursued by Quaglia and Walker through typed barbed equivalences. Merro gives a labeled characterization of barbed-congruences in the asynchronous pi-calculus without matching. Castellani and Hennessy have investigated an asynchronous version of CCS with both may and must testing preorders, as a basis for future work on the theory of testing for the asynchronous pi-calculus.

Various localized asynchronous calculi have also been introduced or examined during last year. The receptive asynchronous distributed pi-calculus of Amadio, Boudol and Loussaine is based on a typing discipline insuring uniform receptiveness. Its expressivity is shown through the coding of standard examples. Safe Ambients is a new theory of Levi and Sangiorgi which provides a nice equational theory for Ambients. The feasibility of a distributed implementation for Ambients has been explored by Fournet, Lévy and Schmitt.

The pi-calculus may also have a symmetric expression through the Parrow and Victor's fusion calculus. Its expressivity is studied by Laneve and Victor. Gardner also shows the connection with action calculi.

The theory of concurrent objects is another important direction of the Calculi area. The aliasing model of Obliq, Ojeblik, demonstrates that several different interpretations exist for the initial Cardelli's Obliq calculus. The objective join calculus is still under development by Fournet, Laneve, Maranget and Rémy. The extension of the pi-calculus with concurrent objects has been published in a journal by Liu and Walker. Finally, Dal Zilio achieved his PhD on the theory of types for objects by using the Boudol's Blue Calculus.

Several more ponctual results may also be mentioned under the Calculi area: Sangiorgi studies CIA (Concurrent Idealised Algol), History-Dependent Automata is a framework for model checking for the finite pi-calculus.
In the area of Logics for Concurrency and the l-calculus, the work has been concentrated this year mainly at ENS and Edinburgh.

Concurrent Games semantics is a new setting introduced by Abramsky and Melliès. Its completeness with respect to the multiplicative additive linear logic has been proved. Danos et al. have connected concurrent games theory with the Ehrhard hypercoherent space model. The duality of call-by-name and call-by-value on one hand, and of input and output on the other hand, is explored by Curien and Herbelin via the Curry-Howard correspondence with the fragments LKT/LKQ of the linear logic. The fragment LKTQ is also considered by Danos. This work surprisingly provides a symmetric and dual lambda-calculus.
Finally, in the area of Programming Languages, progress has been produced in the following directions.

Nomadic Pict is a distributed version of Pierce/Turner's Pict language. Sewell, Unyapoth and Wojciechowski continues their work on the design and semantics. The implementation is now completed. Jocaml (Caml augmented with the join-calculus primitives) has been equipped of a distributed garbage collector (as published in previous Progress Report). At Pisa, Klaim (Kernel Language for Agents Interaction and Mobility) is a prototype language for coordinating processes which run on a net.

ICL explores the downstream use of agent technology with Fujitsu Laboratories, and ICL Businesses. The usage of Facile has been pushed to the Java community by the new availability of MLj (Standard ML compiled to Java) of Microsoft Research. As Facile is written in SML, one easily get the translation of Facile programs to JVM code, and to strengthen the compatibility with other Java programs.
During Year 2 of CONFER-2 two workshops have been held.

The working group has produced about 65 reports and several of these have been published at conferences, international workshops and journals. Many of these works were produced by researchers at different sites within the Working Group and can be stated as state-of-the-art research. They are mainly 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/

Previous Next Contents