Univalent Type Theorems: Models, Equalities, and Coherence
Abstract
Recent breakthroughs in Mathematics and Computer Science are transforming the way in which information is processed, stored, and shared in computer systems. These changes create not only great benefits, but also significant challenges. In particular, the dependency of modern societies on computer systems requires us to ensure that programs behave as they are supposed to do, especially when they handle safety-critical operations, such as transport systems or medical equipment.The proposed research seeks to improve our understanding of the logical theories that underpin important computer systems that are used to guarantee software correctness. These logical theories, called type theories, have been subject of intense research in recent years, thanks to the discovery of unexpected links with topology, an area of pure mathematics which is concerned with the study of the general notions of a space.In particular, we want to investigate further a new type-theoretic axiom, called theUnivalence Axiom, by exploring models of type theories in mathematical structures thatare suciently rich to represent all kinds of spaces. We also wish to establish to whatextent existing type theories can be strengthened with additional axioms for equalitieswithout compromising their good computational properties. Finally, we want to establishmore formly the links between type theory and topology by exploring how certain complexmathematical structures, called low-dimensional categories, can be represented in typetheories.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Sep 11, 2017
- Source ID
- FA95501710290
Entities
People
- Nicola Gambino
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Leeds