The name discipline of uniform receptiveness

In a process calculus, we say that a name x is uniformly receptive for a pr ocess P if: (1) at any time P is ready to accept an input at x, at least as long as there are processes that could send messages at x; (2) the input o ffer at x is functional, that is, all messages received by P at x are appli ed to the same continuation. In the pi-calculus this discipline is employed , for instance, when modeling functions, objects, higher-order communicatio ns, or remote-procedure calls. We formulate the discipline of uniform recep tiveness by means of a type system, and then we study its impact on behavio ural equivalences and process reasoning. We develop some theory and proof t echniques for uniform receptiveness, and illustrate their usefulness on som e non-trivial examples. (C) 1999 Elsevier Science B.V. All rights reserved.