Jonathan Sterling

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory Degree Type: Ph.D. in Computer Science
Advisor(s): Robert W. Harper
Graduated: December 2021

Abstract:

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.

Thesis Committee:
Robert Harper (Chair)
Jeremy Avigad
Karl Crary
Lars Birkedal (Aarhus University)
Kuen-Bang Hou (Favonia) (University of Minnesota)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Dependent type theory, cubical type theory, homotopy type theory, normalization, Artin gluing, logical relations