Modal Homotopy Type Theory in Agda For Modeling Complex Systems
Abstract
The field of interactive proof checking has seen impressive achievements for the past 15 years. Complex software systems, such as a C compiler, have been built in a certified way using such tool; a recent example is a verified optimizer for Quantum circuits [HRH+21]. Another achievement has been the checking of long and sophisticed proofs in mathematics, such as the proof of the 4 color theorem, or Feit-ThompsonÕs result. A common feature of these results is that they have been carried out in systems built on the formalism of dependent types, and used in a crucial way the fact that this formalism allows for a fruitful interaction between reasoning and computations. Indeed, in such systems, the notions of proofs and programs are represented in a uniform way. One recent surprising discovery is that this language of dependent types seems to be also well adapted for expressing some highly abstract notions in mathematics, the notion of ´-topos, connected to homotopy theory and higher category theory. The research proposed here, resting on this new homotopical interpretation of type theory, has for goal to improve existing proof systems. This will allow them to reach new levels of abstraction, while preserving the tight connections with computations. The technical approaches pursued by this effort are: sheaf models of type theory; synthetic algebraic geometry; use and semantics of modalities in type theory; cohesive homotopy type theory. This research should help in developing further the use of computational proof assistants, which can ultimately have a crucial r™le in addressing challenging problems of DoD interest, such as building complex software systems having strong security guarantees.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Oct 07, 2021
- Source ID
- W911NF2110318
Entities
People
- Thierry Coquand
Organizations
- Army Contracting Command
- United States Army
- University of Gothenburg