Contextual Labelled Semantics for Higher-order Process Calculi

In this paper, we study a contextual labelled transition semantics for Higher-Order process calculi. The labelled transition semantics are relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. Besides we develop a novel approach to reason about behaviours of a higher-order substituted process P{Q/X}, based on which we can directly prove a very important result - factorisation theorem. To show the correspondence between our semantics and the well-established ones, we characterize our bisimulation in a version of barbed equivalence.