Grant: Discovery Grants Program - Individual

Historically a branch of algebraic topology, homotopy theory is now its own discipline with deep connections to many other areas, including algebraic geometry, number theory, geometric topology, category theory, and theoretical computer science, among others. My research utilizes the techniques and tools of homotopy theory to establish novel approaches to, and results in, two areas of mathematics: logic, in the form of homotopy type theory, and combinatorics, in the form of discrete homotopy theory. Homotopy type theory is a new approach to foundations of mathematics, pioneered by Fields medalist Vladimir Voevodsky. It is based on the realization that dependent type theory, a formal system suitable for large scale computer implementation, has a natural interpretation in a variety of homotopy-theoretic settings. This suggests possible extensions of the theory by principles inspired by homotopy theory, and the resulting theory is referred to as univalent type theory. My research program seeks to understand the computational and semantic aspects of univalent type theory. My Discovery Grant program will enable the creation of a new generation of computer proof assistants, with strong computational properties and sound mathematical interpretation. Proof assistants are currently used to formally verify correctness of mathematical proofs and programs. They are used widely in industry, e.g., to verify the correctness of cryptographic protocols, operation systems' kernels, and air traffic control systems. The new generation of proof assistants, based on univalent type theory, will transform the way formalization is done. Discrete homotopy theory uses homotopy theory to study graph theory. Graphs, that is, collections of nodes connected by edges, are used to model social and technological networks, and the techniques of discrete homotopy theory have been applied to study their connectivity, e.g., in coordinating rescue missions or assessing how social interactions affect students' academic performance. The area has also been applied to (topological) data analysis, in addition to applications within pure mathematics in areas such as hyperplane arrangements and matroid theory. My work within discrete homotopy theory has two-fold objectives: first, developing computational tools for homotopy-theoretic invariants of graphs, and second, comparing discrete homotopy theory to the classical homotopy theory of topological spaces. The work proposed here will transform the fields of homotopy type theory and discrete homotopy theory. The creation of a new generation of proof assistants will increase the security of Canadian citizens by providing them with reliable software for banking, communication, and transportation. The enhancement of the computational techniques of discrete homotopy theory will give us new tools to analyze large data sets and our social and technological networks.