The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

A good way to start would be
  A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading,

  Beta Ziliani and Matthieu Sozeau
  2015
  http://www.pps.univ-paris-diderot.fr/~sozeau/research/publications/A_Unification_Algorithm_for_Coq_featuring_Universe_Polymorphism_and_Overloading-ICFP15.pdf

This article mostly discusses on the unification algorithm (which is key to many aspects of Coq), but it starts by giving an excellent and up-to-date introduction to the metatheory of CIC.

On Sun, Nov 29, 2015 at 10:04 PM, Talia Ringer <tringer AT cs.washington.edu> 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