The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Thank you, all. I'm borrowing the book from another student, and I'll take a look at the paper as well.

On the implementation side, is anyone familiar with where in the code to start (particularly if I care about definitional equality), or is that a question better suited for the developers?

Thanks again,

Talia

On Sun, Nov 29, 2015 at 1:20 PM, Amirhossein Vakili <avakili AT outlook.com> wrote:

Hi Talia,

With respect to CIC, I found "Type Theory and Formal Proof: An Introduction" by Nederpelt and Geuvers very interesting.

Cheers,
Amir

On 15-11-29 04:04 PM, Talia Ringer wrote:

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