For type checking of functional programming languages, it is fundamental to be able to check equality of types, or in other words, to check whether two types are convertible. This becomes more tricky for dependently-typed languages, since equality of types depends on equality of terms. An important aspect is that this conversion checking algorithm is correct. Since a type theory can be seen as a programming language, a question is whether these aspects about type theory can be proven inside type theory.

In this talk I will present a proof of correctness for a practical conversion checking algorithm for a dependent type theory with one universe à la Russell, natural numbers, and η-equality for Π types. This proof uses a logical relation parameterized by equivalence relations for types and terms. The logical relation is then instantiated twice, once to prove canonicity and injectivity of type formers, and once again to prove completeness of the algorithm. The proof uses inductive-recursive definitions and has been formalized in the proof assistant Agda.