Homotopy Type Theory: Programming and Verification

Lead Research Organisation: University of Leeds
Department Name: Pure Mathematics

Abstract

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-Löf 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.

Publications

10 25 50
publication icon
Awodey S (2017) Homotopy-Initial Algebras in Type Theory in Journal of the ACM

publication icon
Gambino N (2017) On operads, bimodules and analytic functors in Memoirs of the American Mathematical Society

publication icon
Gambino N (2017) The Frobenius condition, right properness, and uniform fibrations in Journal of Pure and Applied Algebra

 
Description My research focuses on new connection between two distant areas of pure mathematics: logic (which studies reasoning) and topology (which studies shapes). The results of my research have improved our understanding of these connections by isolating the essential features that some topological models of the logical systems need to have. This has been done by abstracting away from two known examples (the simplicial and cubical models of type theory), so as to develop a general theory. Further research has focused on obtaining new models of other logical systems using the notion of an operad (which describes a variety of algebraic structures) and on the characterisation of recursive data-types using topological insights.
Exploitation Route One of the goals of my research in the long-term is to guide the implementation of new programming languages and of new software-verification tools, to be applied in safety-critical systems.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://www1.maths.leeds.ac.uk/~pmtng/
 
Description London Mathematical Society Grant Scheme 3 (Joint Research Groups_
Amount £2,000 (GBP)
Organisation London Mathematical Society 
Sector Learned Society
Country United Kingdom
Start 10/2015 
End 10/2016
 
Description US Air Force Office for Scientific Research (AFOSR)
Amount $359,000 (USD)
Funding ID FA9550-17-1-0290 
Organisation US Air Force European Office of Air Force Research and Development 
Sector Public
Country United Kingdom
Start 09/2017 
End 08/2020
 
Description Constructive models of univalent type theories in homotopy types 
Organisation Chalmers University of Technology
Department Department of Computer Science and Engineering
Country Sweden 
Sector Academic/University 
PI Contribution Christian Sattler and Nicola Gambino are investigating the possibility of defining models of univalent type theories that combine the advantages of Voevodsky's simplicial model (i.e. of models supporting all homotopy types) and of Coquand's cubical sets (i.e. of being definable in a constructive meta theory). A promising example is that of prismatic sets, already being considered in the homotopy-theoretic literature.
Collaborator Contribution Investigation of known models of univalent type theories, to check if they support homotopy types.
Impact The project involves both mathematical logic, theoretical computer science, algebraic topology and category theory.
Start Year 2017
 
Description Kleisli bicategories 
Organisation University of Cambridge
Department Department of Biochemistry
Country United Kingdom 
Sector Academic/University 
PI Contribution I have re-started a collaboration with M. Fiore, M. Hyland and G. Winskel on Kleisli bicategories. This has also branched out into a separate project with M. Fiore on the differential lambda-calculus, with the prospect of the submission of an EPSRC grant application.
Collaborator Contribution We wrote a paper accepted for publication in Selecta Mathematica.
Impact The article "Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures" (publications).
Start Year 2016
 
Title Coq code proofs 
Description The proofs of the results in the paper "Homotopy-initial algebras in type theory" have been fully formalised in the Coq proof assistant. The resulting computer code has been submitted with the paper for publication. 
Type Of Technology Software 
Year Produced 2015 
Open Source License? Yes  
Impact No notable impact. 
URL https://github.com/kristinas/hinitiality