Homotopical inductive types

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

Abstract

Over the past few years, new surprising connections have emerged between two traditionally distant areas of mathematics: mathematical logic (which is generally concerned with the study of the forms of reasoning used in mathematics) and homotopy theory (which is interested in understanding and classifying various notions of space). These connections are useful because they provide a clear
geometric intuition that helps us to work with a class of logical systems, known as type theories. On that basis, the Fields medallist Vladimir Voevodsky has formulated an ambitious research programme, called the Univalent Foundations of Mathematics programme, that seeks to develop a new foundations of mathematics on the basis of type theories that include new axioms motivated by homotopy theory.

The proposed research seeks to advance our understanding of the type theories proposed by Voevodsky in order to develop the Univalent Foundations programme. Our first goal is to understand better the relationship between the type theories introduced by Voevodsky and axiomatic set theories, which represent the more traditional approach to foundations of mathematics. In particular, we want to clarify the logical status of the Univalence Axiom, a new axiom which allows us to treat objects that share all structural properties as equal. Furthermore, we wish to gain further insight into a variation, again motivated by homotopy theory, over the standard way of defining types.

Planned Impact

The modern world relies in an essential way on computer systems to run important tasks in a variety of areas: from finance and medicine to transport and energy. When computer systems are used in safety-critical applications (such as controlling the functioning of a nuclear power station or coordinating the signal system of a train network), it is essential that their correctness is established without doubt, and not merely indicated by tests.

One successful approach to the verification of software correctness has been to develop integrated software systems, known as proof assistants, in which it is possible to write computer programs, specify requirements, and formally prove that these requirements hold. Thus, these systems give us a way of creating correct-by-construction programs, which is beneficial also in economic terms since it eliminates the difficult process of debugging. The development of proof assistants involved a combination of ideas of mathematical logic and computer science, in a way that is reminiscent of the very origin of computer programming. Indeed, proof assistants are also used in the formalisation of mathematical proofs, so as to guarantee their correctness.

The proposed research focuses on logical systems, known as type theories, which are at the core of some of the most powerful proof assistants (such as the Coq system). In particular, we seek to advance our understanding of a new class of type theories which have been recently formulated by the Fields medallist Vladimir Voevodsky, thanks to the discovery of surprising connections between
mathematical logic and homotopy theory (an area of mathematics that studies general notions of space).

Our proposed research will benefit directly the academic communities working in mathematical logic, homotopy theory and higher-dimensional category theory by improving our understanding of this new class of type theories and of the connections between these subjects. Our work is likely to impact also the ongoing design of new proof assistants based on these new type theories, since it aims to obtain precise information on their expressive power. These new proof assistants, in turn, will benefit society in general by facilitating the creation of correct-by-construction computer programs.

Publications

10 25 50
 
Description We have developed technical tools for dealing with infinitary
intuitionistic derivations and rextracting computational information from them in the presence of strong axioms such as Powerset and Exponentiation and used them to determine the strength of type theories with the type of propositions.
We also proved several of Feferman's conjectures pertaining to the indeterminacy of iconic set-theoretic statements in semi-intuitionistic set theories.
Exploitation Route They will provide answers concerning the strength of current proof assistants.
Sectors Creative Economy

 
Description Results about the indefinitness of the continuum problem in semi-intuitionistic set theories have stirred a lot of interest in set theory and the philosophy of mathematics.
First Year Of Impact 2014
Sector Other
Impact Types Cultural