Canonicity and Computability in Homotopy Type Theory
Logic in Computer Science
2023-08-21 v1
Abstract
This dissertation gives an overview of Martin Lof's dependant type theory, focusing on its computational content and addressing a question of possibility of fully canonical and computable semantic presentation.
Keywords
Cite
@article{arxiv.2308.09621,
title = {Canonicity and Computability in Homotopy Type Theory},
author = {Dmitry Filippov},
journal= {arXiv preprint arXiv:2308.09621},
year = {2023}
}
Comments
Dissertation submitted in partial fulfillment of a requirement for the degree of Master in Mathematics and Computer Science at University of Oxford