** Next:** Basic properties and types
**Up:** Calculi
** Previous:** Calculi

Boudol introduced the *blue calculus* [Bou97a]. It
proposes a synthesis of the lambda-calculus and the pi-calculus. This
calculus contains a new type system which incorporates both the notion
of functional type and that of sort for communication channels. This
type system has been further studied by Dal-Zilio in [Dal97],
where it is shown to extend naturally to an implicit polymorphic type
system à la ML.

These types only express very weak properties of the behaviour of
processes. For instance, one cannot guarantee the absence of *
deadlock*; here we mean by deadlock that a process calls a resource
that will never become available. To overcome this lack of
expressiveness, G. Boudol has proposed in [Bou97b] a more
refined notion of type, which incorporates a part of Hennessy-Milner
logic: a resource declaration is given a modal type indicating that a
value of a certain type is available on a certain name. This new type
system is shown to enjoy the subject reduction property. This research
will be hopefully extended with a proof that typability implies the
absence of deadlock.

In [Am97] Amadio presents a model of mobility based on the pi-calculus. He relies on an elementary typing, which ensures that in a system, at every moment, to a given name there corresponds a unique resource (whose state can change from one call to another, however). In this way, one can consider a site - or a locality - as a name associated to a resource whose state is either `alive' or `dead'. Amadio develops on this basis a formalism to speak about migration and failures, and he provides reasoning methods which use a notion of bisimulation.

In [RieHen97a] Riely and Hennessy studied in detail location
failure for distributed processes. A language is defined in which
threads are run at distributed locations, and from this a semantic
theory is developed using the basic notions of *observer* and
*experiment* . Roughly, an observer interacts with a distributed
process either by synchronizing with one of its threads or by halting
one of its locations; two programs are equivalent if they present the
same structure of observations, evolving over time. The main result
of this work is to provide an alternative characterization of this
*observational equivalence* which is suitable to automatic
verification. This is done using a temporal logic to characterize the
interdependence between synchronization events and failures.

In [RieHen97b] Riely and Hennessy present a more expressive
language, which includes agent migration, location failure and a rich
system of *capabilities* used to tag communicated data.
Intuitively, when the name, say, of a location is communicated, a set
of capabilities for that location is communicated at the same time;
these may include the capability to read data, to write data, to halt
the location, to migrate to it, or to allocate fresh resources at it.
We present a series of type systems for this language and show,
through examples, that very expressive type systems are necessary in
order to be able to type many important practical programs.

Lavatelli works on the definition of an algebraic semantics of based on approximants, in the flat scenario (where both abstractions and deadlock are observable), which turns out to be sound. Work in progress concerns completeness. The aim is to use these results as intermediate steps in the characterization of the flat semantics through an intersection type system. Another work in progress, by Lavatelli and Curien, concerns the use of techniques of logical relations to compare the inequational theories of two models of that have arisen naturally when trying to give a semantics to .

Now, Parrow and Victor have also developed the update-calculus where
processes can perform *update* actions with side effects, and a
scoping operator controls the extent of the
effects [PV97]. In this way it incorporates
fundamental concepts from imperative languages, concurrent constraints
and from functional formalisms. Structurally it is similar to but
simpler than the pi-calculus; it has only one binding operator and a
symmetry between inpout and output.

Finally, in [SWP97], Sewell, Wojciechowski and Pierce have proposed a simple calculus of agents that can migrate between sites and can interact by both location dependent and location independent message passing. It has a precise reduction semantics. Implementations of the location independent primitives can be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. This allows the algorithms to be stated and understood precisely, a clean implementation strategy for prototype languages (such an encoding can be realized as one phase of a compiler), and reasoning. It also provides a setting in which multiple communication mechanisms can coexist gracefully.

[[Am97]]
R. Amadio.

An asynchronous model of locality, failure, and process mobility.

In *Proc. Coordination 97, Springer Lect. Notes in Comp. Sci.
1282*, 1997.

[[AmCou97]]
R. Amadio and S. Coupet-Grimal.

Analysis of a guard condition in type theory (preliminary report).

Technical Report TR 1997.245. Also RR-3300 INRIA, Université de
Provence (LIM), 1997.

[[Bou97a]]
G. Boudol.

The pi-calculus in direct style.

In *Proceedings POPL'97*, 1997.

[[Bou97b]]
G. Boudol.

Typing the use of resources in a concurrent calculus.

In *Proceedings ASIAN'97, LNCS 1345*, 1997.

[[Dal97]]
S. Dal-Zilio.

Implicit polymorphic type system for the blue calculus.

Technical Report RR-3244, INRIA, 1997.

[[RieHen97a]]
J. Riely and M. Hennessy.

Distributed processes and location failures.

Technical Report 2/97, 1997.

Extended abstract presented at ICALP97.

[[RieHen97b]]
J. Riely and M. Hennessy.

A typed language for distributed mobile processes.

In *Proc. POPL'98, ACM Conference on Principle of
Programming Languages, San Diego*.

[[PV97]]
J. Parrow and B. Victor.

The update calculus (full version).

Technical Report DoCS 97/93, Department of Computer Systems, Uppsala
University, Sweden, Sept. 1997.

Extended abstract to appear in the proceedings of AMAST'97.

[[SWP97]]
Peter Sewell, Pawe T. Wojciechowski, and Benjamin C. Pierce.

Location independence for mobile agents.

Submitted for publication, 1997.