Towards 'up to context' reasoning about higher-order processes.

Proving behavioural equivalences in higher-order languages is a difficult task, because interactions involve complex values, namely terms of the language. In coinductive (i.e., bisimulation-like) techniques for these languages, a useful enhancement is the ‘up-to context’ reasoning, whereby common pieces of context in related terms are factorised out and erased. In higher-order process languages, however, such techniques are rare, as their soundness is usually delicate and difficult to establish.