[TYPES/announce] Fully-funded doctoral studentships in dependently type programming at Oxford and Strathclyde

[Jeremy.Gibbons@comlab.ox.ac.uk]

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 at cs.nott.ac.uk) 
  Neil Ghani (ng at cis.strathclyde.ac.uk) 
  Jeremy Gibbons (jg at comlab.ox.ac.uk)
  Conor McBride (conor at strictlypositive.org)