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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
3
  • $\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 'SO- stop being evil'
    Aug 21, 2014 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$
    – zpavlinovic
    Aug 21, 2014 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, 2014 at 12:28

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.