Skip to main content

Doctoral studentship in Dependently-Typed Programming

Posted: 17th February 2009

A fully funded doctoral studentship is available to work with Jeremy Gibbons in the Algebra of Programming group on the EPSRC-funded project Reusability and Dependent Types. The project is joint with Thorsten Altenkirch in the Functional Programming Laboratory at the University of Nottingham, and Conor McBride and Neil Ghani in the Mathematically Structured Programming group at the University of Strathclyde.

The overall aim of the project is to address the problem that more specific typing information—as for example in dependently-typed programming—often leads to fewer opportunities for reuse. Oxford's particular role is to look at refinement of datatypes, so that more specific types can be expressed as ornamentations imposed upon more general types rather than as completely separate definitions; for example, constraints on length or on element ordering may be layered on top of a standard datatype of lists. The student's work will involve theoretical issues (modelling of ornaments, and of their composition and application), language design issues (convenient expression of these models), and pragmatic issues (case studies exploring patterns of refinement). A possible thesis title might be Refinement of Data Structures in Dependently-Typed Programming.

The studentship is funded by EPSRC for three and a half years, starting from October 2009. The funding covers fees at home/EU level, plus the standard stipend (currently £12,940pa); non-EU students will require supplementary funding. Candidates must have or be expecting to receive a good degree in computer science or a closely related subject, and must satisfy the admissions criteria for doing a doctorate at Oxford.  Previous knowledge of some combination of functional programming, type theory, language design, and formal methods will be an advantage.

Applicants can either apply online or download an offline application form. They will need to submit references, transcript and a statement of research interests (in the field marked "research proposal"). Please quote the studentship code 09COMP-JG-WEB or 09COMP-JG-FIND, if you are applying via or 09COMP-JG-JOBS if you are applying via All applications are subject to a £25 application fee. The closing date for applications is 15th April 2009.