CONFER-2 Working Group
Content:
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.
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.
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:
- 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.
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.
- 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.
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.
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:
- 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.
Clearly new research topics identified in the CONFER BRA
will be addressed in the CONFER-2 working group. These cover:
- 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.
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