This paper presents a Java-like core language with primitives for
object-oriented distribution and explicit code mobility. We apply our
formulation to prove the correctness of several optimisations for
distributed programs. Our language captures crucial but often
hidden aspects of distributed object-oriented programming, including
object serialisation, dynamic class downloading and remote method
It is defined in terms of an operational semantics that
concisely models the behaviour of distributed programs using machinery
from calculi of mobile processes. Type safety is established using
invariant properties for distributed runtime configurations.
We argue that primitives for explicit code mobility offer a programmer
fine-grained control of type-safe code distribution, which is crucial
for improving the performance and safety of distributed
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.