** Next:** Participation to CONFER Workshops
**Up:** INRIA-Sophia
** Previous:** INRIA-Sophia

The notion of *type*, intended in a very general sense as a
``partial specification of the way system components should be used'',
is present, at various degrees, in most of our works this year.

In [Am97] R. 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'. R. 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 [San97a], D. Sangiorgi formulates a type system for mobile processes that guarantees, in a distributed process, that at any moment a given name gives the access to a unique stateless resource. This discipline, called uniform receptiveness, is employed, for instance, when modeling functions, objects, higher-order communications, remote-procedure calls. The impact of the discipline on behavioural equivalences and process reasoning is studied. Some theory and proof techniques for uniform receptiveness is developed, and their usefulness on some non-trivial examples is illustrated.

The work [San97J] is an application of the proof techniques developed in [San97a]. Cliff Jones has proposed transformations between concrete programs and general transformation rules that increase concurrency in a system of objects, and has raised the challenge of how to prove their validity. A proof of correctness of the hardest of Jones's concrete transformations is presented.

The *blue calculus*, introduced by G. Boudol in a POPL'97 paper
[Bou97a], 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 S. Dal-Zilio in [Dal97], where it is shown
to extend naturally to an implicit polymorphic type system à la ML.

However, 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 [PiSa97], parametric polymorphism in message-based concurrent programs is investigated, focusing on behavioral equivalences in a typed process calculus analogous to the polymorphic lambda-calculus of Girard and Reynolds. Polymorphism constrains the power of observers by preventing them from directly manipulating data values whose types are abstract, leading to notions of equivalence much coarser than the standard untyped ones. The nature of these constraints is studied through simple examples of concurrent abstract data types and develop basic theoretical machinery for establishing bisimilarity of polymorphic processes. Some surprising interactions between polymorphism and aliasing are also observe, drawing examples from both the polymorphic pi-calculus and ML.

Another work on mobility [AmPra97] concerns the modelling
of *mobile hosts* on a network in a simple name-passing process
calculus. The protocol considered is a highly simplified version of
proposals for *mobility support* in the version 6 of the Internet
Protocols (IP). We concentrate on the issue of ensuring that messages
to and from mobile agents are delivered without loss of connectivity.
We provide three models of increasingly complex nature of a network of
routers and computing agents that are interconnected via the routers:
the first is without mobile agents and is treated as a specification
for the next two; the second supports mobile agents, and the third
additionally allows correspondent agents to *cache* the current
location of a mobile agent. Following a detailed analysis of the
three models to extract invariant properties, we show that the three
models are related by a suitable notion of equivalence based on *
bisimulation*.

In [AmCou97] we consider the issue of representing
``infinite'' and ``total'' objects like infinite streams or
non-terminating processes in type theory. We present a realizability
interpretation of co-inductive types based on *partial equivalence
relations* (per's). We extract from the per's interpretation sound
rules to type recursive definitions. These recursive definitions are
needed to introduce `infinite' objects of co-inductive type. We show
that the proposed type system enjoys the basic syntactic properties of
subject reduction and strong normalization with respect to a confluent
rewriting system first studied by Gimenez. We also compare the
proposed type system with those studied by Coquand and Gimenez. In
particular, we provide a semantic reconstruction of Gimenez's system
which suggests a rule to type nested recursive definitions.

The final version of the book [AmCu97] has been delivered. The book addresses the mathematical aspects of the semantics of programming languages. The mathematical objects manipulated are order-theoretic structures, and the languages we consider are typed lambda-calculi. The book considers various extensions of typed lambda-calculi to include non-determinism, communication, and concurrency, and it summarizes some of the work carried on in the Confer project.