The formalism of the Coq proof assistant is the calculus of co-inductive constructions. It is a conservative extension of the calculus of constructions that was the upper right back corner of the lambda cube that we saw in the lecture on the proof theoretical foundations. The choice of this logic is the key to the resolution of the apparent contradiction in the de Bruijn principle. This is a logic which has a very simple syntax. Very few typing rules. But still it is extremely powerful. And systems are represented in this logic by using the Curry - Howard isomorphism, where propositions (formulas) are seen as types and proofs are seen as l-terms.

---