** Next:** Workshops, Travels and Visits
**Up:** Università di Bologna
** Previous:** Università di Bologna

**Calculi**- In this area, we have been involved both in the static semantics
(polymorphic type theory) and the dynamic one (analysis of bisimulation)
of concurrent calculi.

**Polymorphic Type Theory**We have studied the adaptation of the Damas-Milner typing discipline to the join-calculus [FLMR97]. Since interactions in the join-calculus are explicitly defined, it turns out that polymorphic types may be effectively inferred as in the lambda-calculus with the let-operator. Our main result is a new generalization criterion that extends the polymorphism of ML to join-calculus definitions. We prove the correctness of our typing rules with regard to a chemical semantics and we also relate typed extensions of the join-calculus to functional languages.

**Analysis of Bisimulation**We have mainly investigated the theory of bisimulation in the join-calculus [BFL97]. To this purpose, we introduce a refined operational model that makes interactions with the environment explicit. In this framework we show that the so-called ``*locality property*'' strongly affects the treatment of bisimulation, and provides a semantics simpler than other proposals in the literature. We also propose several formulations of bisimulation and we establish that all formulations yield the same equivalence, which is finer than barbed congruence. Bisimulation and barbed congruence coincide in the presence of name-testing. **Logics for Concurrency -calculus**- Our research
in this field has been mainly focused on the theory of optimal
sharing in -reduction. In particular, we proved that the
notion of optimal ``parallel'' reduction, as formalized by Lèvy,
is not
*elementary recursive*[AM98]. The result should not be understood in a negative sense: it just says that the notion of optimal sharing*cannot have*a simple implementation since, essentially,*all the computational work*can be done via sharing. Actually, the result is straightforward consequence of the fact that every term of the simply typed lambda calculus can be essentially reduced in a linear number of ``parallel'' (i.e. sharable) -reduction. **Programming Languages**- We proceeded in two
directions, here:
**BOHM**- We are still working on
our implementation of Lamping's graph reduction algorithm
for optimal reduction of functional languages (the Bologna
Optimal Higher-order Machine [AG98]). We have
almost completed a new ``light'' version,
essentially inspired by Girard's Light Linear Logic.
The
*light*version provides a much sharper syntactical control over the shape of sharing graphs than that provided by the rough encoding of intuitionistic implication into linear logic, with a significant impact on the efficiency of the reduction. **Join-calculus**- We have a first prototype of a C
implementation of the distributed join-calculus. This has
been mostly conceived as an implementation exercise, and some
features are still missing (especially in the type system: no
type inference, no polymorphism, no recursive
types, ...). According to our (very preliminary) tests,
the performance looks comparable with the implementation developed
at INRIA (but several optimizations are still missing).

We expect to make a first release for the beginning of 1998.