[Agda] Microsoft PhD Scholarship at Strathclyde

[Conor McBride]

Apologies for crossposting. Please forward this message
to individuals or lists who may be interested. In addition
to the recently advertised PhD position at Strathclyde on
"Reusability and Dependent Types", I am delighted to
advertise the following PhD opportunity.

{---------------------------------------------------------
-- Haskell Types with Numeric Constraints ----------------
---------------------------------------------------------}

We are grateful to Microsoft Research for their
sponsorship of this project, which includes an internship,
and with it the chance to make a real difference to world
of principled but practical programming.

The project investigates the practical and theoretical
impact of extending Haskell's type system with numeric
expressions (representing sizes, or ranges, or costs, for
example) and constraints capturing richer safety
properties than are currently managed by static typing. It
has three strands: (1) to investigate type inference with
numeric constraints, (2) to investigate new programming
structures, patterns, and techniques which exploit numeric
indexing, and (3) to study the performance benefits
derivable from richer guarantees. A bright student could
bring significant benefits to developers using Haskell, a
language with increasing industrial traction — not least
at Microsoft.

Work on the Glasgow Haskell Compiler, at Strathclyde!

{---------------------------------------------------------}

The position is fully funded, covering stipend, fees (at
the home/EU rate), equipment, and travel, starting in
October 2009. The closing date for applications is 15th
April 2009. For further details, see:

   http://personal.cis.strath.ac.uk/~conor/phds/

or email me (conor at cis.strath.ac.uk).

I look forward to hearing from you.

Yours &c

Conor McBride