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-co... 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+Strathc... That's in the centre of Glasgow, Scotland, an amazing place. * We actively seek to promote diversity in our workplace.