Proof techniques for showing that dependent type checking is decidable I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and thus that definitional equality is decidable.

In many references I read, the decidability of typechecking is listed as a corollary of strong normalization, and I believe it in those cases, but I'm wondering how one goes about actually showing this.

In particular, I'm stuck on the following: 


Just because well typed terms are strongly normalizing, doesn't mean that the algorithm won't loop forever on non-well typed inputs
Since logical relations are usually used to show strong normalization, there's not a convenient decreasing metric as we progress typechecking terms. So even if my type rules are syntax directed, there's no guarantee that applying the rules will eventually terminate.


I'm wondering, does anyone have a good reference to a proof of decidability of typechecking for a dependently typed language? If it's a small core calculus, that's fine. Anything that discusses proof techniques for showing decidability would be great.
There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why things work out all right when type-checking in a &quot;standard&quot; dependent type theory (I'll be deliberately vague, since these issues tend to crop up regardless):
Fact 1: If ${\cal D}$ is a derivation of $\Gamma\vdash t:A$, then there is a derivation ${\cal D}'$ of $\Gamma \vdash A:s$ for some kind $s$, and for every subterm $u\leq t$, there is some type $B$, a context $\Delta$ and a derivation $\cal D''$ of $\Delta\vdash u:B$.
This nice fact is somewhat hard to prove, and offset by a pretty nasty counter-fact:
Fact 2: In general, $\cal D'$ and $\cal D''$ are not sub-derivations of $\cal D$!
This depends a bit on the precise formulation of your type system, but most &quot;operational&quot; systems implemented in practice do satisfy Fact 2.
This means that you cannot &quot;pass to sub-terms&quot; when reasoning by induction on derivations, or conclude that the inductive statement is true about the type of the term you're trying to prove something about.
This fact bites you quite harshly when trying to prove seemingly innocent statements, e.g. that systems with typed conversion are equivalent to those with untyped conversion.
However, in the case of type inference, you can give a simultaneous type and sort (the type of the type) inference algorithm by induction on the structure of the term, which may involve a type-directed algorithm as Andrej suggests. For a given term $t$ (and context $\Gamma$, you either fail or find $A, s$ such that $\Gamma\vdash t:A$ and $\Gamma\vdash A : s$. You do not need to use the inductive hypothesis to find the latter derivation, and so in particular you avoid the problem explained above.
The crucial case (and the only case which really requires conversion) is application:
infer(t u):
   type_t, sort_t &lt;- infer(t)
   type_t' &lt;- normalize(type_t)
   type_u, sort_u &lt;- infer(u)
   type_u' &lt;- normalize(type_u)
   if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
      return B, sort_t (or the appropriate sort)
   else fail

Every call to normalize was done on well-typed terms, as this is the invariant for infer's success.

By the way, as it is implemented, Coq does not have decidable type checking, as it normalizes the body of fix statements before attempting to type check them.
At any rate, the bounds on the normal forms of well-typed terms are so astronomical, that the decidability theorem is mostly academic at this point anyways. In practice, you run the type checking algorithm for as long as you have patience for, and try a different route if it hasn't finished by then.