First-Order Reasoning for Higher-Order Concurrency

Abstract

By combining and simplifying two of the most prominent theories for HO! of Sangiorgi et al. and Jeffrey and Rathke [15, 4], we present an effective first-order theory for a higher-order picalculus. There are two significant aspects to our theory. The first is that higher-order inputs are treated in a first-order manner, hence eliminating the need to reason about arbitrarily complicated higher-order contexts, or to use up-to context techniques, when establishing equivalences between processes. The second is that we use augmented processes to record directly the knowledge of the observer. This has the benefit of making ordinary firstorder weak bisimulation fully abstract w.r.t. contextual equivalence. It also simplifies the handling of names, giving rise to a truly propositional Hennessy-Milner characterisation of higher-order contextual equivalence. Furthermore, we illustrate the simplicity of our approach in proving several interesting equivalences by exhibiting first-order witness weak bisimulations, and inequivalences by 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 picalculus.