7
$\begingroup$

I'm learning about language metatheory and type systems, and am using coq to formalize my study. One of the things I'd like to do is examine type systems that include dependent types, which I understand is very involved: being able to rely on coq would be invaluable.

Since this type system feature (and other, simpler ones) brings the expressive power of my studied system closer to coq's own, I worry that I might run into a bootstrapping problem that might not reveal itself until much later. Perhaps someone here can address my fears before I set out.

Can coq express its own metatheory? If not, can it still express simpler systems that include common forms of dependent typing?

$\endgroup$
3
$\begingroup$

It is possible to formalize Coq's logic within Coq but only subsets of the logic have been formalized yet. Relevant contributions are CoqInCoq, PTS, PTSATR, and PTSF.

$\endgroup$
  • $\begingroup$ Is it possible to formalize the whole of Coq's logic within Coq, and not just a subset (possibly a subset that's large enough for many practical purposes)? What precisely to you include in “formalize Coq's logic”? $\endgroup$ – Gilles Aug 21 '14 at 13:58
  • 1
    $\begingroup$ Formalizing Coq's logic would probably mean formalizing Calculus of Inductive Constructions. I would be also interested in what are the major obstacles for formalizing the whole CiC. $\endgroup$ – bellpeace Aug 21 '14 at 17:21
  • 1
    $\begingroup$ I think the only part of Coq that hasn't been formalized yet is the mechanism that introduces (co)inductive and (co)recursive definitions. Keeping Gödel in mind, it should possible to prove, for example, that not having a positivity checker can introduce inconsistencies and that the positivity checker is well implemented. Without this, Coq is practically just ECC, which has already been formalized, and the definitions need to be introduced as axioms or kept as hypotheses. I only listed some formalizations that were easiest to find. $\endgroup$ – Rui Baptista Aug 22 '14 at 12:28

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.