The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> 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?

It is difficult to answer without knowing what you are looking for exactly.

In some sense, definitional equality is pervasive in the
implementation in that reasoning about CIC expressions is most
everywhere done up to βιδζ-conversion.

If however you are specifically looking for where the conversion rule
is implemented in the type-checking kernel (and actually where its
generalization into a subtyping rule is implemented) then, look at
file reduction.ml in directory kernel (internal function
Reduction.ccnv, accessible through different ways, simplest uses being
from Reduction.conv and Reduction.conv_leq). But it is a quite
involved code, relying on a call-by-need evaluation machine itself
having incorporated along the years various fine-tunings (see file
closure.ml). And to understand reduction.ml you may have to look also
at names.ml, constr.ml, term.ml, and various other related files.

More generally, I don't know of anything for Coq like what e.g. the
Matita team did in their "A compact kernel for the calculus of
inductive constructions" paper.

Best,

Hugo

> 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
> 
> 
> 
>