University of Birmingham > Talks@bham > Theoretical computer science seminar > First-Order Reasoning about Higher-Order Concurrency

First-Order Reasoning about Higher-Order Concurrency

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Paul Levy.

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 methodology 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 pi-calculus.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.