Univalent Verification of Parameterized Structures
Abstract
Dependent type theory is a logical formalism commonly used in the formal verification of computer programs and mathematical proofs, and particularly in the development of correct-by-construction typed functional programs. Over the past 15 years, a new interdisciplinary field known as homotopy type theory has emerged from surprising connections between dependent type theory, homotopy theory, and higher category theory, leading to new theoretical insights in all three areas. We propose to develop new foundational techniques for the formal verification of functional data structures in dependent type theory, based on insights from homotopy type theory. These techniques will build upon the Structure Identity Principle and higher inductive types to establish abstraction results known as internal representation independence theorems. In particular, we propose to extend prior work by the PI in order to address theoretical and practical aspects of reasoning about data structures that are parameterized by other structures. We anticipate that our results will reduce the formalization effort required to verify common functional data structures in the Cubical Agda proof assistant, and will increase proof modularity by splitting complex data structure verifications into separate and reusable steps. If time permits, we may also investigate applications of our results to formalized mathematics. Successful completion of this project may contribute to the next generation of language-based techniques for formal verification of critical software systems and large-scale mathematical proofs.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Feb 06, 2025
- Source ID
- FA95502410350
Entities
People
- Carlo Angiuli
Organizations
- Air Force Office of Scientific Research
- Indiana University
- United States Air Force