World's most popular travel blog for travel bloggers.

[Solved]: Can coq express its own metatheory?

, , No Comments
Problem Detail: 

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?

Asked By : phs

Answered By : Rui Baptista

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.

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback