Canonicity and normalisation for Dependent Type Theory
classification
💻 cs.PL
keywords
typecanonicitydependentnotionreducibilitytheoryapproachargument
read the original 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.
This paper has not been read by Pith yet.
Forward citations
Cited by 1 Pith paper
-
Shallow Embedding of Type Theory is Morally Correct
Shallow embedding of type theory into Agda is injective up to definitional equality via a syntactic translation model, with implementation hiding ensuring no illegal propositional equalities arise.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.