Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Resources to learn about CIC metatheory/implementation in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Amirhossein Vakili <avakili AT outlook.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Resources to learn about CIC metatheory/implementation in Coq
  • Date: Sun, 29 Nov 2015 21:20:27 +0000
  • Accept-language: en-CA, en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=avakili AT outlook.com; spf=Pass smtp.mailfrom=avakili AT outlook.com; spf=None smtp.helo=postmaster AT BAY004-OMC2S17.hotmail.com
  • Ironport-phdr: 9a23:WOha1h1WWvTrFx+GsmDT+DRfVm0co7zxezQtwd8ZsegQL/ad9pjvdHbS+e9qxAeQG96LtrQU1aGP7/+ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0oLniavrp8KbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBO/xeL19RrhFBhwnNXo07Yvlr1OLGQCI/z4XVngcuhtOGQnMqh/gCMTfqCz/48N42TOaOtbtQLEyEQqr7KZvSVe8gTkOND898UnQl9B0i6VY5hmmokoskMbvfIiJOa8mLevmdtQASD8ZUw==
  • Spamdiagnosticmetadata: NSPM
  • Spamdiagnosticoutput: 1:23
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


Archive powered by MHonArc 2.6.18.

Top of Page