Computational higher-dimensional type theory
Abstract
Formal constructive type theory has proved to be an effective language for mechanized proof. By avoiding non-constructive principles, such as the law of the excluded middle, type theory admits sharper proofs and broader interpretations of results. From a computer science perspective, interest in type theory arises from its applications to programming languages. Standard constructive type theories used in mechanization admit computational interpretations based on meta-mathematical normalization theorems. These proofs are notoriously brittle; any change to the theory potentially invalidates its computational meaning. As a case in point, Voevodsky's univalence axiom raises questions about the computational meaning of proofs.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 01, 2017
- Source ID
- 10.1145/3093333.3009861
Entities
People
- Carlo Angiuli
- Robert Harper
- Todd Wilson
Organizations
- Air Force Office of Scientific Research
- California State University, Fresno
- Carnegie Mellon University