*Abstract:* We study *mobile systems*, i.e. systems
with a dynamically changing communication topology, from a process
algebras point of view. Mobility can be introduced in process
algebras by allowing names or terms to be transmitted. We
distinguish these two approaches as *first-order* and
*higher-order*. The major target of the thesis is the
comparison between them.

The prototypical calculus in the first-order paradigm is the
*pi-calculus*. By generalising its sort discipline we derive
an *w*-order extension called *Higher-Order
pi-calculus* (HO-pi). We show that such an extension does not
add expressiveness to the pi-calculus: Higher-order processes can
be faithfully compiled down to first-order, and respecting the
behavioural equivalence we adopted in the calculi. Such an
equivalence is based on the notion of bisimulation, a fundamental
concept of process algebras. Unfortunately, the standard definition
of bisimulation is unsatisfactory in a higher-order calculus
because it is over-discriminating. To overcome the problem, we
propose *barbed bisimulation*. Its advantage is that it can
be defined *uniformly* in different calculi because it only
requires that the calculus possesses an *interaction* or
*reduction* relation. As a test for barbed bisimulation, we
show that in CCS and pi-calculus, it allows us to recover the
familiar bisimulation-based equivalences. We also give simpler
characterisations of the equivalences utilised in HO-pi. For this
we exploit a special kind of agents called *triggers*, with
which it is possible to reason fairly efficiently in a higher-order
calculus notwithstanding the complexity of its transitions.

Finally, we use the compilation from HO-pi to pi-calculus to investigate Milner's encodings of lambda-calculus into pi-calculus. We present analogous encodings of lambda-calculus into HO-pi. By comparison with those into pi-calculus, these are easier to understand and with a closer correspondence between reduction on lambda-terms and on their process counterparts. We show that the two encodings of lazy lambda-calculus and the compilation from HO-pi to pi-calculus commute. Thus we can reason in HO-pi and the results hold for pi-calculus as well. In this way we are able to derive a direct characterisation of the equivalence upon lambda-terms induced by Milner's encoding and by the behavioural equivalence adopted on the process terms.

From the representability result of HO-pi in pi-calculus we
conclude that the first-order paradigm, which enjoys a simpler and
more intuitive theory, should be taken as *basic*.
Nevertheless, the study of the lambda-calculus encodings shows that
a higher-order calculus can be very useful for reasoning at a more
abstract level.

*LFCS report ECS-LFCS-93-266 (also published as
CST-99-93)*