First-Order Reasoning for Higher-Order Concurrency

Vasileios Koutavas ( Trinity College Dublin )

Developing effective reasoning techniques for languages with higher-order constructs is a challenging problem, made even more challenging with the presence of concurrency and mobility. In this talk I will present a practical and effective reasoning methdology for such a language, which employs first-order reasoning and handles examples in a straightforward manner. There are two significant aspects to this 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 first-order 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.
I will illustrate the simplicity of the approach with example equivalences and inequivalences, and use it to show that contextual equivalence in a higher-order setting is a conservative extension of the first-order picalculus.

A link to a relevant paper: https://www.cs.tcd.ie/Vasileios.Koutavas/publications/hopitr.pdf