First-order reasoning for higher-order concurrency

We present a practical first-order theory of a higher-order π-calculusπ-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 HOπHOπ of Sangiorgi et al. and Jeffrey and Rathke [10] and [21], 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 equivalences between compact but intricate higher-order processes using witness first-order bisimulations, and proofs of inequivalence using the propositional Hennessy–Milner logic. Finally we show that contextual equivalence in a higher-order setting is a conservative extension of the first-order π-calculusπ-calculus.

► A first-order, fully abstract, theory of standard weak bisimulation equivalence for a higher-order π-calculusπ-calculus.
► A series of compelling example process equivalences.
► The first propositional HML characterisation of weak bisimulation for a higher-order π-calculusπ-calculus.
► We confirm that contextual equivalence in a higher-order setting is a conservative extension of the first-order π-calculusπ-calculus.