Cubical Type Theory: Principles and Practice
Abstract
Intuitionistic type theory is a comprehensive language for the formulation, discovery, and verification of mathematical proofs. A distinctive feature of type theory is that the very constructs used to express mathematics are also used to state and verify the behavior of computer programs. This correspondence gives computational meaning to both mathematical constructions, such as mappings and proofs, and gives mathematical meaning to programming constructions, such as abstract types and functions. These correspondences have inspired the theory of programming languages for decades. Moreover, type theory has emerged as a powerful tool for the verification of programs and proofs. Homotopy Type Theory (HoTT) is an extension of intuitionistic type theory with new concepts that were motivated by consideration of abstract notions of space arising in homotopy theory. It enriches type theory with two new principles: Higher inductive types and Voevodsky’s univalence principle. This project extends the propositions as types principle to account for these homotopy theoretic concepts. A key innovation is the introduction of cubical type theory, which accounts for the higher dimensional aspects of HoTT using an abstract notion of cubes representing evidence for interchangeability in any context. Computational cubical type theory is based on a programming language for specifying and manipulating such cubes, with types being specifications of such programs, thereby connecting homotopy theory with programming language theory.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 14, 2022
- Source ID
- FA95501910216
Entities
People
- Robert Harper
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University
- United States Air Force