Canonicity and normalisation for Dependent Type Theory
Programming Languages
2018-10-23 v1
Abstract
We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back to Godel's Dialectica interpretation and the work of Tait. A key feature of our approach is the use of a proof relevant notion of reducibility.
Keywords
Cite
@article{arxiv.1810.09367,
title = {Canonicity and normalisation for Dependent Type Theory},
author = {Thierry Coquand},
journal= {arXiv preprint arXiv:1810.09367},
year = {2018}
}
Comments
9 pages