A process calculus extending the pi-calculus with higher-order agent a
bstractions as in the Higher-Order Ti-calculus and first-order data ot
her than names but with only first-order interaction is used to give a
natural and direct semantic definition for a concurrent object-orient
ed programming language. A notion of partial confluence of agents is i
ntroduced and its theory developed, first in the setting of CCS and th
en in the mobile-process calculus. It is shown how the semantic defini
tion can be used as a basis for reasoning about systems prescribed by
programs of the language: the theory of partial confluence is used to
prove the indistinguishability in an arbitrary program context of two
classes whose instances combine to form data structures only one of wh
ich supports concurrent operations. (C) 1998-Elsevier Science B.V. All
rights reserved.