Explicit convertibility proofs in pure type systems
Floris van Doorn, Herman Geuvers, Freek Wiedijk · 2013
We define type theory with explicit conversions. When type checking a term in normal type theory, the system searches for convertibility paths between types. The results of these searches are not stored in the term, and need to be reconstructed every time again. In our system, this information is also represented in the term. The system we define has the property that the type derivation of a term has exactly the same structure as the term itself. This has the consequence that there exists a natural LF encoding of such a system in which the encoded type is a dependent parameter of the type of the encoded term.