APAN Community
APAN Community
  • Site
  • User
  • Community  Chat Connect  Maps Translate  Support
  • Site
  • Search
  • User
AFOSR
  • Working Groups
AFOSR
Research Areas Homotopy Type Theory: Unified Foundations of Mathematics and Computation
  • Research Areas
  • Events
  • Upload Report Deliverables
  • Request a No Cost Extension
  • Public File Share
  • Presentations Directory
  • More
  • Cancel
  • New
Join this community to post and share content - click to join
  • -AFOSR Funded Projects
    • Centers of Excellence
    • -Multidisciplinary Research Program of the University Research Initiative (MURI)
      • -Active AFOSR MURI Grants
        • +2018 MURI Grants
        • +2017 MURI Grants
        • +2016 MURI Grants
        • +2015 MURI Grants
        • -2014 MURI Grants
          • A Unified Mathematical and Algorithmic Framework for Managing Multiple Information Sources of Multi-Physics Systems
          • Active Metasurfaces for Advanced Wavefront Engineering and Waveguiding
          • Convergent Evolution to Engineering: Multiscale Structures and Mechanics in Damage Tolerant Functional Biocomposite and Biomimetic Materials
          • Development of Universal Security Theory for Evaluation and Design of Nanoscale Devices
          • Homotopy Type Theory: Unified Foundations of Mathematics and Computation
          • Integrated Quantum Transduction with Photons, Phonons and Spins
          • Plasma-Based Reconfigurable Photonic Crystals and Metamaterials
          • Shedding Light on Plasmon-Based Photochemical and Photophysical Processes
          • Studying Ultrafast Electron Dynamics in Condensed Matter with Next Gen
          • Wiring Quantum Networks with Mechanical Transducers
        • +2013 MURI Grants
      • +Inactive AFOSR MURI Grants
  • +Research Areas
  • +AFOSR Workshops & Reviews
  • +Educational and Special Programs
  • +International Division (Research Areas - International Office)
  • 2018 Joint AFOSR High-Speed Aerodynamics and ONR Hypersonics Programs Annual Review
  • +Special Events and Lectures

Homotopy Type Theory: Unified Foundations of Mathematics and Computation

[Under construction]
2014 AFOSR MURI
Homotopy Type Theory: Unified Foundations of Mathematics and Computation
PO: Dr. Tristan Nguyen, Information Assurance and Cybersecurity
PI: Dr. Steven Awodey, Carnegie Mellon University
Website: 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.

  • Share
  • History
  • More
  • Cancel
Click to hide this icon and message
Select Your Language
  • Support
  • /
  • Hotline: Help Desk 808-472-7855
  • /
  • Privacy
  • /
  • Terms
  • Powered by All Partners Access Network