Research directions

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.