FULLY-FUNDED DOCTORAL STUDENTSHIPS IN DEPENDENTLY-TYPED PROGRAMMING AT OXFORD AND STRATHCLYDE A new EPSRC-funded project on Reusability and Dependent Types has just started, as a collaboration between the Functional Programming Laboratory at the University of Nottingham (Thorsten Altenkirch), the Algebra of Programming group at the University of Oxford (Jeremy Gibbons), and the Mathematically Structured Programming group at the University of Strathclyde (Neil Ghani and Conor McBride). We are all familiar with Milner's slogan that "well-typed programs cannot go wrong". Types express properties of programs; more expressive type systems - such as dependent typing - can state properties more precisely, providing stronger guarantees of behaviour and additional guidance in development. However, this expressivity comes at a price: more specific typing can reduce opportunities for code reuse. The goal of this project is to investigate techniques for promoting reuse without sacrificing precision; in particular, how can we layer dependently typed programs, imposing stronger invariants onto more general library code? Two fully-funded doctoral studentships are available to work in this area: one at Oxford (with JG) and one at Strathclyde (with CTM). Each covers stipend, fees (at the home/EU rate), equipment, and travel, and is for three and a half years from October 2009. The closing date for applications is 15th April 2009. For further details, see: http://web.comlab.ox.ac.uk/news/72-full.html http://personal.cis.strath.ac.uk/~conor/phds/ or contact one of the principal investigators on the project: Thorsten Altenkirch (txa@cs.nott.ac.uk) Neil Ghani (ng@cis.strathclyde.ac.uk) Jeremy Gibbons (jg@comlab.ox.ac.uk) Conor McBride (conor@strictlypositive.org)