Type Theory for Data-Intensive Formalization
Abstract
In our research we will design and implement new techniques for formal verification of mathematics that will improve the capabilities of the state-of-the-art proof assistants by making them more flexible and easily adaptable to user needs. We will also advantageously combine libraries of formalized mathematics with large databases of mathematical structures. We shall apply mathematical formalization methods to large databases of mathematical structures, with the objective to provide high-grade assurance of their correctness, and to enable new methods of exploration and analysis. We shall incorporate the databases into proof assistants, so that they are readily available for heuristic checking of statements, automatic generation of hypotheses, and guidance of proof search. For this purpose, we will develop domain-specific type theories that are tailored to the content and structure of mathematical data, such as type theories for graph theory, finite groups, or combinatorics. We will design and implement transformations between type theories that will allow the databases to be interfaced with proof assistants and other tools for formal reasoning. The domain-specific type theories will have other uses in formalized mathematics as well. They can be used to express auxiliary notions of type theory, such as universe levels and induction schemata, and to give modular and reusable implementations of automated reasoning algorithms. A second goal of the project is the development of novel type systems for programming languages with low-level real-world computational effects that exhibit asynchronous, stochastic, or even quantum-mechanical behavior. We shall adapt and extend algebraic effect systems, which have so far been used successfully to describe computational effects as a programming technique for implementation of effects within a language.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 21, 2022
- Source ID
- FA95502110024XX0
Entities
People
- Andrej Bauer
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Ljubljana