Sterling_Jonathan.pdf (1.62 MB)
Download file

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory

Download (1.62 MB)
thesis
posted on 27.04.2022, 16:55 by Jonathan SterlingJonathan Sterling

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 Air Force

Find out more...

FA95501910216

FA9550211009

History

Date

01/10/2021

Degree Type

Dissertation

Department

Computer Science

Degree Name

  • Doctor of Philosophy (PhD)

Advisor(s)

Robert Harper