Dependent types and program equivalence
Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich · 2010
The definition of type equivalence is one of the most important design issues for any typed language. In dependently typed languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for the term equivalence relation.