Advanced dependent type system

The use of advanced functional programming languages and techniques has long held out the possibility for a step change in terms of security and reliability in programming. This has progressed with the development of advanced dependent type systems not only to capture complex functional specifications, but which can also be used to encode low-level details of data layout and representation.

This research will investigate leveraging these techniques towards being able to achieve levels of efficiency and performance on par with (and even beyond) mainstream languages whilst retaining the architectural benefits and safety guarantees of functional programming languages. Such an approach would potentially have applications in performance critical, real time systems such as medical devices and video games. Our initial focus will target recent developments in homotopy type theory, specifically the use of so-called higher inductive types in data representation, which support the ability to 'add equations to data', and hence to consider a programmer-driven theory of optimisation.