This thesis turns to semantics, giving a definition of the core language (with a type system) and proving correctness of an example infrastructure. This involves extending the standard semantics and proof techniques of process calculi to deal with the new notions of sites and agents. The techniques adopted include labelled transition semantics, operational equivalences and preorders (\eg. expansion and coupled simulation), ``up to'' equivalences, and uniform receptiveness. We also develop two novel proof techniques for capturing the design intuitions regarding mobile agents: we consider translocating versions of operational equivalences that take migration into account, allowing compositional reasoning; and temporary immobility, which captures the intuition that while an agent is waiting for a lock somewhere in the system, it will not migrate.
The correctness proof of an example infrastructure is non-trivial. It involves analysing the possible reachable states of the encoding applied to an arbitrary high-level source program. We introduce an intermediate language for factoring out as many `house-keeping' reduction steps as possible, and focusing on the partially-committed steps.