The Coq mailing list

[Maxime Dénès <Maxime.Denes AT inria.fr>]

Hello Chantal,

Chapter 3 of Bruno Barras' thesis should be a good match ;) You can 
download it from his homepage, although it seems unreachable at the moment.

Roughly speaking, the conversion test is implemented by interleaved 
reduction steps and term comparisons (as opposed to the VM which goes 
straight to normal form). The reduction is performed by a call by need 
abstract machine.

Hope it helps.

Maxime.

On 17/10/2012 17:28, Chantal Keller wrote:
> Dear Coq club,
>
> I am looking for information about the "standard" Coq's kernel reduction
> mechanism. By this, I mean the mechanism involved in the conversion rule
> when doing "Qed." (in usual proofs, ie. when the VM is not called). Can
> you give me a pointer on its working?
>
> Thanks,