Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: Canonical Structure

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Canonical Structure


chronological Thread 
  • 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 Gonthier
(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 ?


Are you talking to me?

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



Archive powered by MhonArc 2.6.16.

Top of Page