Bisimulations

In [BFL98], Boreale, Fournet and Laneve developed a new theory of bisimulation for the join calculus. They consider open terms, and define two bisimulations, weak and asynchronous, both refinments of the observational equivalence. This gives a more compositional sense to the interaction of the terms of the join-calculus with contexts, and is a start point to logical systems for reasoning on join-terms.

More generally, many equivalences have been proposed for process algebra for the study of convergence, security or fairness. Gonthier started a comparison of equivalences used both in the pi and join calculus, mostly based on reduction semantics, observation of barbs and preservation by contexts. Many variants appear according to the way these elementary constructs are combined. But fortunately many lead to a same result. One shows that fair-testing is connected to coupled bisimulation, or that omega-limit bisimulation is also related to single-barb gfp bisimulation. This provides new proof techniques and a better understanding of process calculi. An article is in preparation, the work has been presented at the Confer Workshop in Amsterdam [Gon98].

Sewell has studied the semantics of PICT in [Sew97c], and has shown how the behaviour of implementations of the language relates precisely to the labelled transitions of the $\pi$-calculus. His results indicate that there is an essentially unique behavioural equivalence appropriate for PICT, from the large space of choices in the literature.

In [Ra97a] an axiomatic characterisation of both late and early observational congruence for a class of fully parameterised processes is given. This result uses a new derivation rule which is an intuitive generalisation of unique fixpoint induction based on loop invariants for symbolic graphs. In the same paper it is shown that the new rule can actually be derived from existing formulations of unique fixpoint induction for value-passing calculi.

In [Ra97b] a first order modal mu-calculus is described which uses parameterised maximal fixpoints to describe safety and liveness properties of value-passing processes. A proof system for deciding if a process satisfies a formula is presented. Certain deduction rules of the system carry side conditions which leave auxiliary proof obligations of checking properties of the value language. Although the proof system is in general incomplete two completeness results are given for significant sub-logics.

Abadi (DEC/SRC), Fournet and Gonthier studied secure implementation of communication in the join calculus. It is easy to write secure protocols when lexical scope is guaranteed, but one needs cryptographic means to enforce a secure lexical scope discipline. By compositionality, two protocols can be considered: one based on the redefinition of secure emission/reception primitives, another one based on firewalls for some locations. The correctness proofs use bisimulation techniques. A presentation by Fournet has been made at the DARPA workshop on Foundations for Secure Mobile Code, March 26-28 mars in Monterey [Fou97], and at the Confer meeting in Amsterdam. An article is in preparation [AFG98].

[[AFG98]] M. Abadi, C. Fournet, and G. Gonthier.
Secure implementation of channel abstractions.
To be submitted for a conference, November 1997.

[[BFL98]] M. Boreale, C. Fournet, and C. Laneve.
Bisimulations in the join-calculus.
Submitted for a conference, September 1997.

[[Fou97]] C. Fournet.
Security within a calculus of mobile agents?
April 1997, http://www.cs.nps.navy.mil/research/languages/statements/fournet.ps.

[[Gon98]] G. Gonthier.
On asynchronous barbs, simulations, and fair testing.
Submitted to a conference, Octobre 1997.

[[Ra97a]] J. Rathke.
Unique fixpoint induction for value-passing processes.
In Proc. LICS'97, 12^th Annual Symposium on Logic in Computer Science, Warsaw. IEEE Computer Society Press, 1997.
To appear.

[[Ra97b]] J. Rathke and M. Hennessy.
Local model checking for value-passing processes.
In Proc. TACS'97, International Symposium on Theoretical Aspects of Computer Software, Sendai. Springer-Verlag, 1997.

[[Sew97c]] Peter Sewell.
On implementations and semantics of a concurrent programming language.
In Proceedings of CONCUR '97. LNCS 1243, pages 391-405. Springer-Verlag, 1997.