Higher Algebra in Computer Science
Abstract
The introduction of homotopy-theoretic methods to dependent type theory has been a major advance in the field, radically changing our understanding of the nature of constructive equality and leading to new techniques, computational principles and research directions. Far from mere theoretical curiosities, these ideas have implications not only for the formalization of mathematics, but also for the design of programming languages and proof-assistants for formally verified software development. This proposal seeks to follow up on and expand the use of homotopy theory and higher algebra in computer science by (1) investigating new type theories which extend and surpass those currently available (2) proposing formalization projects which test the limits of these theories and (3) continuing the study of the natural semantics of these theories. Objective 1 Identify and implement new classes of type theories with computational univalence. Objective 2 Investigate extensions of type theory able to define coherent higher structures. Objective 3 Develop methods to reason internally about the meta-theory of dependent type theory. Objective 4 Test these theories by formalizing ideas from higher algebra and homotopy theory. Objective 5 Deepen our understanding of higher topos theory, a natural semantics of type theory.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Feb 22, 2024
- Source ID
- FA95502310029
Entities
People
- Eric Finster
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- University of Birmingham