Today, people and businesses are reliant on computer systems everyday for a variety of services ranging from healthcare, banking, travel, communications etc. When these systems fail, the consequences are staggering on multiple levels, severely affecting the society and the economy of countries. In the UK, in 2018 alone, there were several high-profile failures: more than 30m O2 users (ranging from delivery companies to London transit authority) in the UK lost access to data services after a software glitch in Ericsson equipment; millions of TSB customers lost access to their online bank accounts after a failed software upgrade; NHS Wales was temporarily unable to access patient data; processors from Intel were found to be vulnerable to attacks where sensitive data could be stolen. The consequences of systems failures are only bound to be more severe in the future, as more and more aspects of our lives will be organised by automated systems such as self-driving vehicles. There is thus a pressing need for reliable and secure computer systems implementing the functionality we depend on in our daily lives. This includes the software, hardware the software is running on and the mathematical algorithms underlying the software.
Computer tools, so-called "computer proof assistants" can help reasoning about the correctness of mathematical algorithms, of software, and of models of hardware. Different languages have been developed as a foundation for such tools, and a several proof assistants have been developed that check the correctness of user-provided proofs. So far, computer proof assistants of different kinds have been used to check the correctness of a wide range of results, from pure mathematics (eg, Kepler Conjecture, Feit-Thompson Theorem) to practical computer systems (eg, C compiler CompCert, certified ML implementation CakeML, and certified micro operating-system seL4).
The language that forms the basis of many of today's computer proof assistants is "type theory". Recent advances in the understanding of type theory have led to the development of a wealth of variations and extensions of the original type theory -- extensions by domain-specific language constructions, such as guarded type theory, cohesive type theory, and many others. These extensions are analogous to domain-specific programming languages, with built-in primitives to construct, and reason about, mathematical objects of a specialized mathematical domain.
Whenever a language is proposed as the foundation of a computer proof assistant, a translation from that language into a world of mathematical objects needs to be specified. Giving this translation rigorously is thus part of proving a mathematical statement in a computer proof assistant. However, it requires much work full of technical details, and thus is rarely done with sufficient care.
A significant obstacle here is the lack of 'modularity' results for syntax extensions of type theory: when reasoning about an extension of a core syntax, for which a translation has already been established, it should be possible to specify a translation on the extended syntax by only specifying it on the extension - thus reusing the work of translating the core syntax. However, there is no mathematical theory for 'extending a translation' to an extended syntax: currently, whenever a new type theory is conceived, a translation has to be specified from scratch.
In light of the plethora of new type theories currently being designed, there is hence a pressing need for a mathematical framework for the specification of, and reasoning about, type theories, with a particular focus on modularity.
This is why we aim, in this project, to develop a mathematical theory of type theories that encompasses the type theories currently used in computer proof assistants. In the long term, we envision a proof assistant whose underlying type theory is configurable via an implementation of our mathematical theory.
|