The strength of functional programming is in its support for abstraction through function composition and abstract data types. Concurrency becomes necessary in dealing with, e.g., distributed and parallel systems.

There is an increasing need for programming tools that provide much better support than presently available for (a) developing complex systems which operate in distributed environments, and (b) for fully exploiting the computing power offered by parallel processors. It is clear that these problems will greatly benefit from the combined strength of functional and concurrent computation.

Theoretical developments in these two areas have previously tended to diverge or at least proceed separately. The divergence is manifest in the obscurity of certain programming languages which attempt to combine the two paradigms without the support of well understood theoretical foundations. A certain amount of diversity is to be expected among calculi that emphasise different aspects of computation.

However, an integral part of the project is to eliminate accidental diversity and to exhibit clearly the relationship between approaches that differ for good reason.

The CONFER project officially started September 1st 1992 with a planned duration of 3 years.

The CONFER action is organised around four main areas of work:

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

In the following sections we give a brief report on the objectives and activities in each area listed above.

In the area of Foundational Models and Abstract Machines the state of the art in basic calculi with bound variables, ranging from the lambda-calculus to higher-order communication systems, has been advanced significantly. Work in the area is often based on the concept of Lafont's interaction nets. The area includes more general schemes such as combinatory reduction systems and abstract reduction systems. The notion of action structures developed by Milner gives an algebraic setting which covers many of the known calculi of communication systems. It seems to allow connections with the very atomic operations of the lambda-calculus.

It treats calculi with bound variables in many ways. Many of the frameworks of this area of CONFER are graph reduction systems; the most highly developed are for functional calculi and provide insight into the optimality of computation strategies, but there are also graphical treatments of the pi-calculus.

Work is going on in the areas of optimal reductions, abstract reduction systems, explicit substitutions, CRS, cyclic CRS, and again action structures.

In the Calculi area, a great deal of work has focused on comparing new calculi with existing ones. This has yielded a better understanding of the expressive power of existing calculi.

Decisive steps have been taken to advance the state of the art in calculi to account for phenomena such as true concurrency and physical distribution, which are of paramount importance for the programming language area.

Since the area of Calculi is rather large we have divided it into three subareas:

- Comparing name passing with agent passing. One of the main objectives is to understand the relationship between name passing, as found in the pi-calculus and to some extent in the concurrent constraint paradigm, and agent passing as found in the lambda-calculus as well as in higher order process calculi such as CHOCS and HO-pi.
- Algebraic theories, model checking and tool. The area of name passing calculi has matured to a state where sound and complete axiomatisations for bisimulations, and even a verification tool has emerged. Moreover, the notion of bisimulation has been extensively studied. Several approaches have been compared, and some of them have been shown to lead to the same notion.
- Adding physical distribution. One of the main motivations for studying concurrent and functional systems is the use in distributed systems.

It is convenient to distinguish three main topics.

The division should not obliterate the connections between the various topics: for instance some works on ``non-interleaving semantics'' show that the pi-calculus is expressive enough to encode these semantics within the standard bisimulation approach. The work on ``relating calculi'' is also concerned with proofs of properties of processes.

- Bisimulations. The well-known notion of bisimulation equivalence, due to Milner and Park, provides a semantics for the class of calculi where the agents' behaviour consists in performing actions along with state transitions. Moreover, the notion of bisimulation provides a very powerful proof technique for establishing properties of agents. This proof technique is implemented in software verification tools that can be used to perform sophisticated verifications.
- Non-interleaving semantics. The non-interleaving semantics was developed for CCS-like process algebras with the idea that a semantics reducing parallel composition to sequential non-determinism is not entirely appropriate for dealing with distributed systems, that are supposed to run on decentralised systems. On the other hand, a clear advantage of the standard approach is its nice mathematical theory, allowing for rigorous proofs of properties of concurrent systems. An obvious direction of research was then to investigate the meaning of non-interleaving semantics for higher order calculi. One may distinguish two different approaches to the non-interleaving semantics: the causal approach, where concurrency is regarded as causal independence, and the saptial approach, where concurrency is given by the distributed nature of a system.
- Relating calculi. Various calculi for higher order communicating processes have been proposed so far, and an obvious task was to investigate their relationships. As a matter of fact, this comparison should also include sequential models of computation.

In the area of Logics for Concurrency and the lambda-calculus, Interaction Categories have been developed as a new foundation for semantics of sequential and concurrent computation. A significant number of studies showing this have been carried out. Several sort and type systems have been developed. These are important for both the correctness and the optimisation of concurrent/functional programs. The work on Linear Logic and Optimality transfers techniques from the lambda-calculus paradigm to concurrency. The work done clearly reflects the fruitful interplay between logic, concurrency, and functional computation.

We have been able to develop type systems for processes, based on principles derived from the work on Interaction Categories, to address issues in synchronous and asynchronous concurrent computation, verification of concurrent systems and mobility. These are non-trivial applications of the Interaction Category paradigm. There has been much work based on Linear Logic, Girard's LU and Categorical Logic as a basis for typed frameworks of processes. Game Semantics and Linear Logic have been used to advance the state-of-the-art in the theory of functional computation.

In the area of Programming Languages several prototypes have been developed: Prototype compiler for lambda-calculus, based on graph reduction, Portable, unobtrusive garbage collection for multiprocessor systems, Lilac: a prototype functional programming language based on Linear Logic, Typed higher-order programming language based on pi-calculus, all deriving from the substantial work on calculi, foundational models and logic. Important work results for compile time optimisations have been obtained on Termination properties of unfolding extended to programs with non-determinism. Clearly some of the above results and prototypes are necessarily of a rather preliminary nature. One exception is the Facile programming language, which is already being experimented with in quite significant applications.

Concrete results from this area have also started to emerge. There is now an advanced implementation of PICT and some demonstration programs have been developed.

The semantic foundation of important techniques on compile time optimisations via unfolding of programs has been studied. This work continues previous activities regarding termination properties of unfolding. The latest results are expected to be mature enough to be applied in prototype compilers.

A programme of research -- the Geometry of Implementations -- aimed at developing efficient implementations of functional programs based on Girard's Linear Logic and the Geometry of Interaction semantics has been initiated. This work is derived from previous CONFER results on optimal reduction implementations and the work on local and asynchronous beta-reduction.

The Calumet demonstrator written in Facile has been developed into a robust application running on wide area networks.

The first release of Facile -- the Facile Antigua Release -- has been announced on the news net and made available for research and educational purposes. Technology transfer to the ECRC shareholders has also taken place

The proposed working group will continue along the four work areas defined in the CONFER BRA:

- Calculi: to develop the theory of those calculi already proposed, to determine their expressive power and to develop systematically their interrelation.
- Foundational Models and Abstract Machines: to develop common platforms for semantics and for implementations.
- Logics for Concurrency and the lambda-calculus: to further develop logics for stating properties of and reasoning about systems
- Programming Languages: the design and experimental implementation of practical programming languages combining concurrency and the lambda-calculus.

- multiple communication paradigms and their coexistence, possibly using action structures and/or interaction categories.
- true concurrency, locality, failure, causality, in the semantics of distributed concurrent functional languages.
- types for programming safety and crucial information about implementation optimisations.
- non-deterministic optimal beta reductions.
- physical distribution, with introduction of locations inside the communication calculus.
- the use of concurrent functional languages in the construction of reliable distributed systems.
- verification, including bisimulation equivalences and formal logics for higher order communication.

These studies will be the grounds for more applicative research, only possible beyond the scope of this working group. The CONFER-2 working group will be the place where smaller projects could be identified and further proposed as Esprit projects, for instance in verification tools, in programming languages and environments for mobile distributed programs, in the building of large distributed applications, etc.

One of the main goals of the CONFER-2 working group is to maintain the community of researchers of the CONFER BRA, with the adjunction of 2 new sites: University Sussex, where there is a strong tradition of studies in concurrency (Hennessy), and France Telecom (CNET-Lannion), which will be a valuable interface with applications.

Furthermore, results of the CONFER BRA have been used in several major European Union sponsored basic research actions and working groups, such as LOMAPS 8130, CONCUR2 7166 and Semagraph II 6345. We expect that the results of the CONFER-2 working group will be of use for these projects and others in the future as well as upcoming industrial RTD projects.

We expect that with the involvement of two industrial partners, ECRC and France Telecom, as well as two national research centres, INRIA and CWI, results produced in the CONFER-2 working group will be exploited industrially as soon as they emerge.

Page maintained by Andrea Asperti