next up previous contents
Next: Workshops, Travels and Visits Up: Università di Bologna Previous: Università di Bologna


The research activity in Bologna, organized along the main task of the Working Group, has been the following:

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 $\lambda$-calculus
Our research in this field has been mainly focused on the theory of optimal sharing in $\beta$-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) $\beta$-reduction.

Programming Languages
We proceeded in two directions, here:
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.
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.

next up previous contents
Next: Workshops, Travels and Visits Up: Università di Bologna Previous: Università di Bologna