First-order reasoning for higher-order concurrency

We present a practical first-order theory of a higher-order pi-calculus which is both sound and complete with respect to a standard semantic equivalence. The theory is a product of combining and simplifying two of the most prominent theories for HOpi of Sangiorgi et al. and Jeffrey and Rathke [13, 6], and a novel approach to scope extrusion. In this way we obtain an elementary labelled transition system where the standard theory of first-order weak bisimulation and its corresponding propositional Hennessy-Milner logic can be applied. The usefulness of our theory is demonstrated by straightforward proofs of equiv-alences between compact but intricate higher-order processes using witness first-order bisimulations, and proofs of inequivalence using the propositional Hennessy-Milner logic. Beyond HOpi, our technique is applicable to other languages, including languages with distribution. In support of this claim we outline how our first-order theory can be easily adapted to model located higher-order processes, in which names can be locally scoped