coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Resources to learn about CIC metatheory/implementation in Coq

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Resources to learn about CIC metatheory/implementation in Coq
Date: Sun, 29 Nov 2015 13:04:16 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-yk0-f180.google.com
Ironport-phdr: 9a23:f+k1bxQWChaEdHyIZTVIc2uUndpsv+yvbD5Q0YIujvd0So/mwa64YBeN2/xhgRfzUJnB7Loc0qyN4/2mCTJLuMrd+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8CVM1sD3WbhKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxyZBBwnMpCv7WJj8qGOuqvB83iaXJ+X9VvYrUC+i7qFkVBjuzioLKmhqoynslsVsgfcD81qarBtlztuMbQ==

Hello,

I have a side project I'm doing for fun right now, and I'd like to learn more about the Coq metatheory (both the CIC metatheory and how it is implemented in Coq). In particular, I want to learn more about definitional equality in Coq, but I assume a whole-picture understanding is helpful. I've already read Adam Chlipala's post on equality. Now I would like to dig much deeper.

Are there any resources that may be helpful? From the CIC side, I am looking for some accessible introductory reading. From the Coq side, I am wondering where in the source code to dig; I've cloned the repository, but I don't know where to start.

Thank you,

Talia

[Coq-Club] Resources to learn about CIC metatheory/implementation in Coq, Talia Ringer, 11/29/2015
- Re: [Coq-Club] Resources to learn about CIC metatheory/implementation in Coq, Gabriel Scherer, 11/29/2015
- Re: [Coq-Club] Resources to learn about CIC metatheory/implementation in Coq, Amirhossein Vakili, 11/29/2015