CONFER-2 Working Group


Content:


Background: The CONFER Basic Research Action

The purpose of the CONFER BRA is to bring together and further develop theoretical foundations and applications of two fundamental computational paradigms of computer science: functional programming and concurrency. The two paradigms apply naturally to different classes of problems.
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:
In the following sections we give a brief report on the objectives and activities in each area listed above.

Foundational Models and Abstract Machines

The objective is to develop common platforms for semantics and for implementations. This will provide a mathematically sound basis and as a consequence provide links between semantics and abstract machines as well as between models and implementations.

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.

Calculi

The objective is to develop the theory of those calculi already proposed, to determine their expressive power and to develop systematically their interrelation. Calculi extract the essence of computational models and provide an algebraic framework for studying basic constructs. We may find that the development of further calculi is necessary, especially in the direction of either adding communication and concurrency primitives to the lambda-calculus or constructing original concurrent calculi that have the lambda-calculus as subcalculus. The latter approach will provide answers to questions in the related area of automatic parallelisation of the lambda-calculus.

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: A large amount of work done in the area of Calculi mainly deals with the semantics of the pi-calculus and other related formalisms.
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.

Logics for Concurrency and lambda-calculus

The objective is to further develop logics for stating properties of and reasoning about systems. One direction is the construction of modal and temporal logics for specification and reasoning about behaviours. Another direction is the development of type systems based on Intuitionistic Logic or Linear Logic using the Curry-Howard isomorphism paradigm. Furthermore concurrent constraints and their connection with Linear Logic and (higher order) mobile processes will be pursued.

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.

Programming Languages

The objective is the design and experimental implementation of practical programming languages combining concurrency and the lambda-calculus. We envision languages supporting features that have been and will be intensely studied, including higher order functions and processes, polymorphism and constructs for communication and concurrency. Such features support a more declarative approach in addressing the various issues that arise in software engineering, especially in such applications as distributed systems, parallel programming, and dynamic connectivity between systems in large and possibly heterogeneous computing environments. Developing languages in a systematic fashion and in close relationship with work proceeding in comparatively more theoretical areas will ensure that languages have a sound mathematical foundation. Strong formal foundations are in turn necessary for developing systems with reliable and verifiable behaviour, reliable compilers and strategies for program transformation in parallelising compilers. Programming languages based on concurrency and the lambda-calculus enable programmers to write applications for dynamically changing systems and demonstrate potential industrial impact of this new programming paradigm. Experiments with implementations and usage of programming constructs will also provide feedback and stimulus for further investigation at the level of calculi and abstract machines. Examples of issues where a better understanding appears to be needed, in both a mathematical and implementational sense, are primitive constructs and the treatment of failures in distributed environments. The construction of applications will likely expose weaknesses in the languages and thus provide feedback and stimulus for the previous objective.

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

Objectives of CONFER-2

Higher order communication is now a very active field of research. Its interaction with functional paradigms has been the central theme of the CONFER BRA. The integration of concurrency and functions has proved to be very useful in the construction of large scale highly reliable and dependable distributed systems. It furthermore shows promising for construction of mobile systems. Thus the development of distributed information systems and mobile information devices is a strong motivation for making tools which ease their programming. The work of the CONFER BRA and the CONFER-2 working group will be necessary for furthering the understanding of the semantics and design of these new tools.

The proposed working group will continue along the four work areas defined in the CONFER BRA: Clearly new research topics identified in the CONFER BRA will be addressed in the CONFER-2 working group. These cover: The proposed work relates to several areas of the European Union R&D Information Technology Programme (Esprit), in particular the area of Software Intensive System Engineering, Task 1.3 and 1.5 and the area of Distributed Systems and Database Technology, Task 1.13 and 1.16.

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