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

<p>Chapter 2 of <a href="https://www.cis.upenn.edu/~bcpierce/attapl/">Advanced Topics in Types and Programming Languages</a>: <em>Dependent Types</em>, David Aspinall &amp; Martin Hofmann.</p>

<p>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.</p>

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

CC BY-SA 3.0
2016-08-02T01:44:54.893Z
2016-08-02T01:44:54.893Z
cody
<p>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?</p>

CC BY-SA 3.0
2016-07-30T13:48:57.967Z
Possibly a duplicate of this question: http://cs.stackexchange.com/questions/41192/algorithmic-type-checking-for-calculus-of-inductive-constructions though the latter doesn't explicitly mention a proof of decidability (the references give proofs though)
cody
CC BY-SA 3.0
2016-07-30T19:56:02.830Z
There are a number of references linked there, do you know which in particular has the proof?
Shea Levy
CC BY-SA 3.0
2016-07-30T22:44:51.123Z
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
<type-theory><decidability><calculus-of-constructions>
Proof of decidability of type checking of calculus of (co)inductive constructions?
Shea Levy
# Proof of decidability of type checking of calculus of (co)inductive constructions?

(Asked by: username_0 on 2016-07-30)

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?

**Tags:** type-theory, decidability, calculus-of-constructions
> **Comments:**
> **username_1**: Possibly a duplicate of this question: http://cs.stackexchange.com/questions/41192/algorithmic-type-checking-for-calculus-of-inductive-constructions though the latter doesn't explicitly mention a proof of decidability (the references give proofs though)  
> **username_0**: There are a number of references linked there, do you know which in particular has the proof?  
> **username_1**: 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.  

---

## 1 answers

### Answer by username_1 on 2016-08-02. Score: 5 | Accepted 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](https://www.cis.upenn.edu/~bcpierce/attapl/): *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.


---

