Foundations of Type Theory for Computation and Mathematics
Abstract
Type theory is a framework used in both computer formalization of mathematics and the designof secure and reliable software systems. We will develop and study a general notion of typetheories which subsumes several major variants, including Martin-Lof type theory and homotopytype theory. We will prove general fundamental theorems about type theories, which have manypotential applications and are commonly believed to hold, but have hitherto only been proved forseveral key instances. We will make sure that our theorems and proofs are complete and free oferrors by formalizing them in a proof assistant (a computer program that helps prove theorems andverifies proofs in complete detail).We will also develop a general theory of transformations between type theories. Such transformations can be used either by proof assistants to translate formalized mathematics from one theory to another, or by type-directed compilers to guarantee that program code is correctly compiled and optimized. We shall devise design principles that allow a proof assistant to be augmented with user-defined transformations, thereby allowing the users to effectively extend existing proof assistants to new type theories.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Sep 11, 2017
- Source ID
- FA95501710326
Entities
People
- Andrej Bauer
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Ljubljana