**Work Area:** Theories for Concurrency and Real Time: Specification and Verification

**Keywords** *integration of functional and concurrent computation, calculi, foundational models, abstract machines, logics, programming languages, parallel and distributed systems*

**Start Date:** 1 September 92 / **Duration:** 36 months / **Status:** Continuing

[ participants / contact ]

**Abstract** CONFER aims at bringing together the area of functional and concurrent computation both in theory and in practice. The two paradigms apply naturally to different classes of problems: functional programming supports abstraction and compositionality, concurrency becomes necessary in dealing with distributed and parallel systems. The objective is to create the concrete basis for using the strength of the two models in rendering more efficient development of systems requiring complex data manipulation as well as distributed computing and exploitation of parallelism. This will require substantially advancing the current state of the art of technologies for formalisation, programming and compiler construction.

The main goal is to create the basis for uniting the two areas of functional and concurrent computation. We shall bring together these two paradigms of computer science both in theory and in practice. The main objectives are the areas in which coordinated research is needed, and in which major advances in technology can be expected by this Consortium:

*Foundational Models and Abstract Machines*- to develop common platforms for semantics and for implementations.*Calculi*- to develop the theory of those calculi already proposed, to determine their expressive power and to develop systematically their interrelation.*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.

The cooperation between partners is organised around a number of concrete themes: *sorts and types, dynamic behaviours, foundational models for mobility, abstract machines and efficient implementations, proofs and processes, primitive constructs, programming languages: implementations and experience*. Each theme addresses issues that span across several or all the main objectives of the action. In addition, two or more of the partners have both clear expertise and a direct interest in each theme. In many cases this has already resulted in collaborations. In the original plans for the project a number of specialised workshops was anticipated. However, instead of having specialised workshops on specific themes we have found that general workshops with sessions devoted to specific topics are of more use at this stage of the project. Apart from the participation in workshops the interaction between partners is based on exchanges of researchers.

We perceive experimental work as an integral part of the project in the sense that it can contribute to verify the feasibility, potential impact and industrial viability of solutions proposed by theory, while simultaneously providing constant feedback and stimulus for theoretical work.

The first year of CONFER has been very successful. The objectives set forth in the work plan have been achieved, and significant results have been obtained beyond these objectives.

Basic calculi with bound variables, ranging from the Lambda-calculus to higher-order communication systems, have been advanced significantly (combinatory reduction systems, abstract reduction systems, action structures) and have lead to optimality of computation strategies. Graphical treatments of the pi-calculus have also been obtained.

Calculi for name passing and for concurrency have matured and been compared. This gives insight for studying true concurrency and physical distribution. Furthermore, a verification tool has been constructed.

The studies of logics (in particular linear logic) have produced insight into optimality for the Lambda-calculus, for concurrent computations, for typing mobile processes. Interaction Categories have been developed as a new foundation for semantics of sequential and concurrent computation.

Several prototype compilers have been developed, including compilers for optimal reductions, linear programming languages and the pi-calculus. The Facile programming language compiler effort has been pursued and is now at a stage where quite significant applications have been constructed.

Systems that involve concurrent computations, thus typically distributed and parallel systems, are well known as difficult to conceive, design, implement and maintain. If one takes a close look at this area of computing technology one has the distinct impression that it is still a bit of a black art. Attempts to use fourth generation programming technology have so far not produced satisfactory results. The fact remains that in most cases problems of distribution and parallelism are attacked with second generation programming techniques.

This project aims at creating the concrete basis to advance the state of the art to a point where technologies of formalisation, programming and compiler construction will allow distributed and parallel systems to be developed with much greater efficiency in terms of both development effort and utilisation of computing resources. It is quite conceivable that the results of this basic research action could constitute the basis for an industrially more focused project in a later stage (Type A, Type B, or Eureka).

The involvement of four research laboratories outside academia - CWI, INRIA, ECRC and SICS - strengthens the opportunities for transferring know how to the European industry. In particular, ECRC is an industrial research centre. Technology transfer to its shareholder companies is an integral part of its mission and has been quite successful so far.

- Pierce B and Sangiorgi D
*Typing and Subtyping for Mobile Processes*Proc. of 8th LICS Conference, Montreal (1993) - Milner R
*Action calculi, or concrete action structures,*Proc. of MFCS Conference, Gdansk, Poland, LNCS 711 (1993) - Danos V and Régnier L
*Local and Asynchronous Beta-Reduction*Proc. of 8th LICS Conference, Montreal (1993) - Gay S J
*A sort inference algorithm for the polyadic, pi-calculus*Proc. of POPL'93 (1993) - Ong L
*Non-determinism in a functional setting,*Proc. 8th LICS Conference, Montreal (1993) - D. Doligez and G. Gonthier,
*Portable, Unobtrusive Garbage Collection for Multiprocessor Systems},*To appear in Proc. of POPL'94 (1994)

The project has the following score at international conferences: 5 papers at LICS (92-93), 3 papers at POPL (93-94), 4 papers at CONCUR (93), 2 papers at TAPSOFT (93), 3 papers at MFCS (92-93), 4 communications at the REX (93) summer school, and 2 PhDs (92-93).

**Coordinator**

INRIA Rocquencourt - F

Domaine de Voluceau

B.P. 105

F - 78153 LE CHESNAY

**Partners**

ECRC GmbH - D

CNRS - ENS - F

INRIA Sophia Antipolis - F

Università di Pisa - I

Centrum voor Wiskunde en Informatica - NL

Swedish Institute of Computer Science - S

University of Edinburgh - UK

The Imperial College of Science, Technology and Medicine - UK

Dr. J.-J. Levy

tel +33/1 39 63 56 89

fax +33/1 39 63 53 30

e-mail: levy@margaux.inria.fr

*CONFER - 6454, August 1994*

*
please address enquiries to the ESPRIT Information Desk
*

html version of synopsis by Nick Cook