# Proof of decidability of type checking of calculus of (co)inductive constructions?

I often see it asserted that type checking is decidable for CIC, but I haven't seen it proven. Is there a good paper (or simple demonstration) of this?

• Possibly a duplicate of this question: cs.stackexchange.com/questions/41192/… though the latter doesn't explicitly mention a proof of decidability (the references give proofs though) – cody Jul 30 '16 at 13:48
• There are a number of references linked there, do you know which in particular has the proof? – Shea Levy Jul 30 '16 at 19:56
• As far as I know, there is no proof for CIC itself. But Randy Pollack's paper proves the decidability for PTSes. The proof carries over to the more complex systems essentially unchanged. – cody Jul 30 '16 at 22:44

## 1 Answer

I found another reference that goes through a detailed proof of the decidability of typechecking for systems of dependent types up to the CIC:

Chapter 2 of Advanced Topics in Types and Programming Languages: Dependent Types, David Aspinall & Martin Hofmann.

As you probably know, the proof of decidability is conditional on decidability of $\beta$-equality, which itself is implied by the normalization of the calculus.

The proof of that statement is significantly more difficult, partly because it implies consistency of the logical system.