Higher algebraic type theory
Abstract
The proposed work consists of two distinct but related components- Higher algebraic type theory (Anel-Awodey), and Computational type theory (Harper). Higher algebraic type theory. The interpretation of dependent type theory using homotopy types, or infinity-groupoids, in Homotopy type theory suggests the possibility of a type theoretic framework for infinity-categories. Such a constructive foundational system will vastly extend the scope of the tools already under development in Homotopy type theory, namely the possibility of formal verification and the computational applications. We will tackle this problem by generalizing the framework of Algebraic type theory, an axiomatization of the natural models of the PI Awodey, from infinity-groupoids to infinity-categories. This research will be jointly conducted by the PI Awodey and Postdoctoral Investigator Mathieu Anel, a leading expert on higher category and topos theory. Computational type theory. This proposed research extends in two directions, integrating cost and behavior in type theory, and investigating a coinductive formulation of equivalence in type theory. In the former, dependent type theory provides an expressive framework for expressing behavioral (correctness) properties of functional programs through a combination of equational reasoning and the use of type structure to express specifications. We will amass further examples and extend them to account for methods such as probabilistic algorithms whose efficiency depends on randomization. We will also investigate a reformulation of univalence in which equality is defined inductively as the least reflexive relation, and equivalence is defined coinductively as the greatest relation between elements of a universe such that the two types can be seen to be equivalent by a contractible map or a biequivalence. This universal characterization provides a more satisfying account of equivalence of types than that originally given by Voevodsky.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 06, 2024
- Source ID
- FA95502310434
Entities
People
- Steve Awodey
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University
- United States Air Force