coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
- To: Fran�ois Garillot <francois.garillot AT inria.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Re: Canonical Structure
- Date: Thu, 20 May 2010 09:58:19 +0200
François Garillot wrote:
On Thu, 18 Mar 2010 15:37:12 +0000, Georges GonthierAre you talking to me?
(gonthier AT microsoft.com)
said in
gmane.science.mathematics.logic.coq.club:4636 :
Like most of the rest of Coq, there is no real documentation of the
inner workings of Canonical Structures, other than the system code;
they are not covered in Coq'art, but I know Yves is cooking up some
kind of tutorial going over some of the design patterns that have
emerged from our work.
By the way, is there something looking like a rough (possibly 'hoped')
timeframe on this work ?
For now, I only found the time to make a few experiments, but I am not sure I understood enough to write a documentation yet. I have no hope of finishing anything before the end of the summer.
Yves
- [Coq-Club] Re: Canonical Structure, François Garillot
- Re: [Coq-Club] Re: Canonical Structure, Yves Bertot
Archive powered by MhonArc 2.6.16.