6
$\begingroup$

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?

$\endgroup$
3
  • 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, 2016 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, 2016 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, 2016 at 22:44

1 Answer 1

5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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