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?

  • 1
    $\begingroup$ 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) $\endgroup$ – cody Jul 30 '16 at 13:48
  • $\begingroup$ There are a number of references linked there, do you know which in particular has the proof? $\endgroup$ – Shea Levy Jul 30 '16 at 19:56
  • 1
    $\begingroup$ 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. $\endgroup$ – cody Jul 30 '16 at 22:44

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.