On Equivalence and Canonical Forms in the LF Type Theory

Robert Harper, Frank Pfenning

Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of defi…