[Under construction]2014 AFOSR MURIHomotopy Type Theory: Unified Foundations of Mathematics and ComputationPO: Dr. Tristan Nguyen, Information Assurance and CybersecurityPI: Dr. Steven Awodey, Carnegie Mellon UniversityWebsite: TBD
RESEARCH PROBLEM AND TECHNICAL APPROACHES: This proposal will enable a tightly knit group of experts in logic, mathematics, and computer science to pursue a recent theoretical breakthrough that is reshaping the foundations of those disciplines. Homotopy type theory is a fundamentally new direction with powerful new principles of reasoning and new, higher-dimensional data types not previously available in set theory or extensional type theory. Its applications range from allowing mathematicians to work with the “right” notion of equality for mathematical structures to offering flexible new generic programming techniques that facilitate the development of certified software. The proposed research will extend the formal foundations of homotopy type theory, further develop its semantics, and study its computational properties. It will also extend formal libraries and computational methods used by computational proof assistants being developed on this basis. This will facilitate the large-scale formalization of logic and mathematics, with far-reaching practical implications for mathematics and information science. The feasibility of this new approach was demonstrated during a special year at the Institute for Advanced Study (Princeton) in 2012–13, the leading participants of which are assembled here into a MURI team. They are uniquely positioned to advance this research program, solving critical open problems and addressing specific issues identified during the IAS year in a proven, effective collaboration.
ANTICIPATED OUTCOME AND IMPACT ON DOD CAPABILITIES: If successful, newly discovered algorithms to support the new foundation will further its application to pure and applied mathematics and computation. Existing computational proof assistants will be enhanced, and new ones developed, leading to their future wide-spread use and remaking foundations into a practical tool for mathematicians. The resulting large-scale formalization of logic and mathematics will enable the creation of powerful scientific tools with impact on challenging problems of DoD interest. The “geometric” intuition underlying this approach provides promising new methods for formalization, reducing the gap between formal and informal proofs, and enabling synthetic approaches to disciplines that would otherwise be difficult to formalize. Moreover, a computational interpretation of homotopy type theory will provide the first account of higher-order computable functions on higher-dimensional spaces and categories, with promising applications to verified mathematical computations and to software verification. As this new foundation becomes better understood and implemented, it has the potential to revolutionize our understanding of the relation between mathematics and computation, and to underlie the development of powerful, practical tools for the working scientist in fields farther removed from pure mathematics such as hardware and software verification, cyber-security, artificial intelligence, robotics, and human-computer interaction.