First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory
The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits
the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type
checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics. In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine
to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the
theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic
metatheory of cubical type theory: normalization of open terms.
Funding
HOMOTOPY TYPE THEORY: UNIFIED FOUNDATIONS OF MATHEMATICS AND COMPUTATION
United States Department of the Air Force
Find out more...FA95501910216
FA9550211009
History
Date
2021-10-01Degree Type
- Dissertation
Department
- Computer Science
Degree Name
- Doctor of Philosophy (PhD)