[Agda] Strathclyde PhD Position

[Conor McBride]

Applications are welcome from ANYWHERE for a Microsoft Research
sponsored PhD position in the Mathematically Structured Programming
group at the University of Strathclyde.

Project:                  Real World Data with Dependent Types:
                            Integrity and Interoperation
Strathclyde supervisor:   Dr Conor McBride
Microsoft supervisor:     Dr Don Syme
Starting:                 October 2015
Tuition fees:             fully funded or substantially subsidised,
                            depending on residency status
Stipend:                  £14,057K
Contact:                  Conor, by 8 May 2015

--------------------------------------------------------------------
Project Summary

Data integrity, manipulation and analysis are key concerns in modern
software, for developers and users alike. We are often obliged to work
with a corpus of files – spreadsheets, databases, scripts – which
represent and act on aspects of data in some domain. This project
seeks to improve the integrity and efficiency with which we can
operate in such a setting by

* delivering a language for data models which expresses their
  conceptual structure, capturing what kinds of things exist in a
  given context, what data we expect to have about them, and when
  those data are consistent;

* delivering a language for data views relative to a model,
  characterizing the expected content of a particular spreadsheet or
  database, whether considered a data source or an output;

* exploiting the descriptions of models and views to support a richer
  tool chain for data editing, auditing, integration and analysis,
  whether by internal spreadsheet calculation or database query, or by
  interfacing with programming languages;

* exploring the art of the possible in automating the discovery of
  views and models from extant data.

Dependent type systems provide a uniform formalism for the
contextualisation of data and the characterization of its
consistency. They use types both as a data representation language and
as a logic, and they do so in a manner amenable to mechanical
checking. However, the prescriptive dependent type systems of Coq,
Agda or Idris are not yet attuned to the open enumerations and
extensible record types that we need to build up models of a data
domain in a compositional, descriptive way.

This project thus offers a broad spectrum of activity, encompassing
theoretical innovation, language design, and tool development in
support of existing applications and programming languages, notably
Excel and F#.
--------------------------------------------------------------------

Small Print

* More detail about the problem and the approach envisaged can be found
  in this blogpost
    https://pigworker.wordpress.com/2015/04/09/model-the-world-view-your-data-control-their-chaos/
  and in these slides
    https://personal.cis.strath.ac.uk/conor.mcbride/dependent-up.pdf

* Our hope is that the student will seek to undertake a paid
  internship at Microsoft Research, Cambridge, at some point during
  the PhD.

* We are based here:
    https://www.google.co.uk/maps/place/Torre+Livingstone,+University+of+Strathclyde,+16+Richmond+St,+Glasgow+G1+1XQ/@55.8611055,-4.2435337,17z/
  That's in the centre of Glasgow, Scotland, an amazing place.

* We actively seek to promote diversity in our workplace.