The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Thanks Maxime, that was exactly what I was looking for.

Perhaps a short description of this reduction would be useful in the
reference manual.

Thank you again,



Le 17/10/2012 17:34, Maxime Dénès a écrit :
> 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,
> 

-- 
Chantal KELLER