Computing Laboratory
Oxford University
2.30pm Tuesday 10 June 2003
Room 2511, JCMB, King's Buildings
We introduce recent approaches to give algorithmic representations of fully abstract game models of (Algol-like) higher-order procedural languages. For lower-order fragments, they give rise to procedures for deciding observational equivalence and other behavioural properties. In the talk, we will survey recent decidability and undecidability results, identify several open problems, and present an ongoing EPSRC-funded research programme at Oxford to investigate applications to program analysis and verification.