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?
$\begingroup$
$\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$– codyCommented 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 LevyCommented 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$– codyCommented Jul 30, 2016 at 22:44
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
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.
