Distributed language features form an important part of modern objectoriented
programming. In spite of their prominence in today’s computing environments,
the formal semantics of distributed primitives for object-oriented languages
have not been well-understood, in contrast to their sequential part. This
makes it difficult to perform rigorous analysis of their behaviour and develop
formally founded safety methodologies. As a first step to rectify this situation,
we present an operational semantics and typing system for a Java-like core language
with primitives for distribution. The language captures the crucial but often
hidden concerns involved in distributed objects, including object serialisation,
dynamic class downloading and remote method invocation. We propose several
invariant properties that describe important correctness conditions for distributed
runtime behaviour. These invariants also play a fundamental rˆole in establishing
type safety, and help bound the design space for extensions to the language. The
semantics of the language are constructed modularly, allowing straightforward
extension, and this is exploited by adding primitives for direct code distribution
to the language: thunk passing. Typing rules for the new primitives are developed
using the invariants as an analysis tool, with type soundness ensuring that their
inclusion does not violate safety guarantees.