The project aims to develop verification techniques for functional programming languages such as Ocaml, F# and other members of the ML family of programming languages. It is anticipated that the scholar will work on one or more of the following tasks:

1. Derive an algorithm for deciding observational equivalence (of an appropriate fragment of Reduced ML) by reduction to the equivalence of visibly pushdown automata, and to build a prototype implementation of it.
2. Develop a notion of reachability test for higher-order procedural languages, and identify language fragments for which it is decidable and determine its complexity.
3. Construct algorithms that symbolically compute over-approximations of an appropriate collecting semantics for higher-order procedural languages, with a view to the data and control flow analysis of these programs.

Each Microsoft scholar will be awarded a bursary of up to 33,000 euros per year up to a maximum of three years. (The amount is the maximum Microsoft Research will pay the University of Oxford - the actual amount payable to the scholar is yet to be determined; see the terms and conditions.) The award will be made automatically the following years after the first, provided the scholar meets the requirements of the university. In addition, every scholar will receive a laptop from Microsoft Research with a selection of software applications.

During the course of their PhD, scholars will be invited to Microsoft Research Cambridge for a summer school that includes a series of talks of academic interest and a poster session, which will give the scholars the opportunity to present their work to Microsoft researchers and a number of Cambridge academics (for example, see the programme of the 2007 Summer School).

Some of the scholars may also be offered, in Microsoft Research's sole discretion, an internship in one of the Microsoft Research laboratories. Internships will involve working on a project alongside and as part of a team of Microsoft researchers. Students will be paid during their internship on top of their scholarship bursary.

More information on OUCL can be obtained from here and informal queries about the project can be sent to Luke.ong@comlab.ox.ac.uk.

For more information about the work of Professor Luke Ong, see his home page.