Projects

Doctoral Training Partnership (DTA - University of Strathclyde) | Dunne, Kevin: Duncan, Ross (Principal Investigator) Ghani, Neil (Co-investigator) Dunne, Kevin (Research Co-investigator); Period 01-Oct-2014 - 01-Apr-2018
Doctoral Training Grant | Andjelkovic, Stevan: McBride, Conor (Principal Investigator) Ghani, Neil (Co-investigator) Andjelkovic, Stevan (Research Co-investigator); Period 01-Oct-2011 - 01-Apr-2015
Homotopy Type Theory: Programming and Verification: Ghani, Neil (Principal Investigator) McBride, Conor (Co-investigator); "The cost of software failure is truly staggering. Well known individual cases include the Mars Climate Orbiter failure (£80 million), Ariane Rocket disaster (£350 million), Pentium Chip Division failure (£300 million), and more recently the heartbleed bug (est. £400 million). There are many, many more examples. Even worse, failures such as one in the Patriot Missile System and another in the Therac-25 radiation system have cost lives. More generally, a 2008 study by the US government estimated that faulty software costs the US economy £100 billion annually. There are many successful approaches to software verification (testing, model checking etc). One approach is to find mathematical proofs that guarantees of software correctness. However, the complexity of modern software means that hand-written mathematical proofs can be untrustworthy and this has led to a growing desire for computer-checked proofs of software correctness. Programming languages and interactive proof systems like Coq, Agda, NuPRL and Idris have been developed based on a formal system called Martin Type Theory. In these systems, we can not only write programs, but we can also express properties of programs using types, and write programs to express proofs that our programs are correct. In this way, both large mathematical theorems such as the Four Colour Theorem, and large software systems such as the CompCert C compiler have been formally verified. However, in such large projects, the issue of scalability arises: how can we use these systems to build large libraries of verified software in an effective way? This is related to the problem of reusability and modularity: a component in a software system should be replaceable by another which behaves the same way even though it may be constructed in a completely different way. That is, we need an extensional equality which is computationally well behaved (that is, we want to run programs using this equality). Finding such an ty is a fundamental and difficult problem which has remained unresolved for over 40 years. But now it looks like we might have a solution! Fields medallist Vladimir Voevodsky has come up with a completely different take on the problem by thinking of equalities as paths such as those which occur in one of the most abstract branches of mathematics, namely homotopy theory, leading to Homotopy Type Theory (HoTT). In HoTT, two objects are completely interchangeable if they behave the same way. However, most presentations of HoTT involve axioms which lack computational justification and, as a result, we do not have programming languages or verification systems based upon HoTT. The goal of our project is to fix that, thereby develop the first of a new breed of HoTT-based programming languages and verification systems, and develop case studies which demonstrate the power of HoTT to programmers and those interested in formal verification. We are an ideal team to undertake this research because i) we have unique skills and ideas ranging from the foundations of HoTT to the implementation and deployment of programming language and verification tools; and ii) the active collaboration of the most important figures in the area (including Voevodsky) as well as industrial participation to ensure that we keep in mind our ultimate goal -- usable programming language and verification tools."; Period 01-Apr-2015 - 31-Mar-2019
Implementing Units of Measure in Haskell: Ghani, Neil (Principal Investigator); Period 01-Jun-2014 - 30-Sep-2015
CORCON (FP7 IRSES): Ghani, Neil (Principal Investigator) Kupke, Clemens (Co-investigator) McBride, Conor (Co-investigator); Period 01-Jan-2014 - 31-Dec-2017
Logical Relations for Program Verification: Ghani, Neil (Principal Investigator); "In an economy as relentlessly digital as the modern worldwide one, in which everything from toasters to interpersonal communications to global financial services are computerised, the need for formally verified software cannot be overestimated. Formal verification uses mathematical techniques to prove that programs actually perform the computations they are intended to perform (e.g., that text editors really do save files when a SAVE command is issued or that automatic pilots really do correctly execute flight plans) and also avoid performing unintended ones (e.g., leaking credit card details or launching nuclear weapons without authorisation). Since programmers make 15 to 50 errors per 1000 lines of code, and since repairing them accounts for some 80% of project expenses, the ever-increasing size and sophistication of programs makes formal verification increasingly critical to modern software development. Mathematical reasoning lies at the core of all formal verification, and so is crucial for building truly secure and reliable software. One of the key techniques for formally verifying properties of software systems uses logical relations. Logical relations provide a means of deriving properties of a software system directly from the system itself; as a result, they can be used to prove important properties of programs, programming languages, and language implementations. Logical relations have been developed for core fragments of many modern programming languages and verification systems. They are currently extended to richer programming languages and properties by constructing plausible variants of the definitions of logical relations for appropriate core fragments and checking that the mathematical theory goes through. But as languages and properties to be proved have become increasingly sophisticated and expressive, this ad hoc approach has become both difficult and unsustainable. It has also led to an enormous constellation of complicated and non-reusable logical relations that work for particular language features, rather than their principled and transferrable development from fundamental principles. In short, logical relations have struggled to keep pace with developments in programming languages, with the obvious consequences for security and reliability of software systems. We aim to revolutionise the landscape of logical relations by providing framework for their development and use that is principled, conceptually simple, reusable, and uniform (rather than ad hoc). Our framework will be capable of both describing the wide array of logical relations already used in existing applications and prescribing new logical relations for future ones. It will be based on the mathematical concept of comprehension for a fibration, which has not previously been identified as a key ingredient in the construction of logical relations. Our use of it thus distinguishes our framework from all other treatments of logical relations in the literature. Comprehension allows explicit representation of logical properties of languages within those languages themselves. This means that our framework will be implementable, so we will produce a logic for deriving consequences of logical relations and a prototype implementation of that logic in a modern interactive theorem prover. This will allow users to experiment with our framework, and allow their experiences with it to feed back into its foundations. We will also apply our new framework for logical relations to cutting-edge problems that are the focus of active research and for which there is presently no consensus on the way forward. Successful application of our framework will show that it can solve problems that are the focus of active research, as well as open up unanticipated new research directions. Conversely, the practical applications we pursue will raise challenges that prompt us to further refine its foundations"; Period 30-Sep-2013 - 29-Sep-2017

more projects

Address

Computer and Information Sciences
Livingstone Tower

Location Map

View University of Strathclyde in a larger map

University of Strathclyde

My Saved Pages

My Saved Courses

Recently visited

Professor Neil Ghani

Head Of Department

Computer and Information Sciences

Prizes and awards

Publications

Projects

Address

Location Map