Basic properties and types

In [San97a], 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.

In [PiSa97], Pierce and Sangiorgi investigate parametric polymorphism in message-based concurrent programs, 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.

Philippou and Walker looks at confluence properties: in a process setting, the essence of confluence is that the occurrence of one action may not preclude others. In the case of $\pi$-calculus, where names may be extruded from their scopes, care is needed to find the right definition. Basic results on confluence in $\pi$-calculus are presented in [PW97] and [P97phd]. In particular, conditions under which combinations of confluent, or almost-confluent, processes yield confluent systems are presented.

In [LW97b], a theory of partial-confluence of processes is developed, in CCS and in $\pi$-calculus. The main theorem concerns systems which can be thought of as composed from two components: a questioner, and an answerer which may process questions concurrently. It gives conditions under which a system of this kind is behaviourally indistinguishable from the corresponding system in which the answerer may handle only one question at a time. This result, together with a semantic definition of the kind described above, is used to show the interchangeability in an arbitrary program context of two class definitions which prescribe binary-tree symbol-table data structures, one supporting concurrent operations, the other sequential.

In [NS97], Nestmann and Steffen also investigates confluence properties for concurrent systems of message-passing processes. In order to prove confluence for a given system, one has to demonstrate that for all states reachable by computation from the starting state, the 'flowing together' of possible computations is possible. However, it is possible to prove confluence properties for concurrent systems without having to generate all reachable states by use of a type system that supports a static analysis of possible sources of non-confluence. One may statically check the occurrences of critical situations by reducing them to the concurrent access on a shared communication port. For the technical development, one focuses on the setting of a polarized pi-calculus, whith the notion of port-uniqueness being formalised by means of overlapping-free context-redex decompositions.

Finally, in [Sew97a], Sewell considers global/local typing. In the design of distributed programming languages, there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. In [Sew97a] a static type system for a distributed $\pi$-calculus is introduced, in which the input and output capabilities of channels may be either global or local. This may allow compile-time optimization, but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly.

[[LW97b]] X. Liu and D. Walker,
Partial confluence of processes and systems of objects,
Theoretical Computer Science B, to appear.

[[NS97]] U. Nestmann and M. Steffen.
Typing confluence.
In S. Gnesi and D. Latella, editors, Second International ERCIM Workshop on Formal Methods in Industrial Critical Systems (Cesena, Italy, July 4-5, 1997), pages 77-101. Consiglio Nazionale Ricerche di Pisa, 1997.
Also available as report ERCIM-10/97-R052, European Research Consortium for Informatics and Mathematics, 1997.

[[PW97]] A. Philippou and D. Walker,
On confluence in the $\pi$-calculus,
in Proceedings of International Colloquium on Automata, Languages and Programming, Bologna, July 1997, Springer-Verlag Lecture Notes in Computer Science, vol. 1256, 314-324.

[[PiSa97]] B. Pierce and D. Sangiorgi.
Behavioral equivalence in the polymorphic pi-calculus.
In 24th POPL. ACM Press, 1997.

[[San97a]] D. Sangiorgi.
The name discipline of receptiveness.
volume 1256 of Lecture Notes in Computer Science. Springer Verlag, 1997.
Full paper available electronically as ftp://zenon.inria.fr/meije/theorie-par/davides/Receptiveness.ps.Z.

[[Sew97c]] Peter Sewell.
Global/local subtyping for a distributed $\pi$-calculus.
Technical Report 435, Computer Laboratory, University of Cambridge, August 1997.
Available from http://www.cl.cam.ac.uk/users/pes20/.