Bisimulation Congruences for Homer: a Calculus of Higher Order Mobile Embedded Resources

We extend Howe's method for proving that late labelled transition
bisimulations are congruences to a core process passing calculus with
local names, extended with non-linear active process mobility
and nested locations, as found in the Seal calculus,
M-calculus, and Kell-calculus. The calculus we consider, called Homer
for Higher-order Mobile Embedded Resources, has a very simple syntax
and semantics, which conservatively extend the standard syntax and
semantics for process passing calculi. The extension of Howe's method
gives a sound characterisation of barbed bisimulation congruence in
terms of a late contextual bisimulation. We show that early contextual
bisimulation is complete with respect to barbed bisimulation
congruence, but that the late bisimulation is in fact strictly
included in the early bisimulation. We discuss the issue of scope
extension through location boundaries in detail, in particular the
difference between fresh name generation and static local
names. We propose free name extension as a primitive
construct in calculi with non-linear process mobility, explicit
locations and local names.