The Coq mailing list

[Giuseppe Castagna <Giuseppe.Castagna AT ens.fr>]

On Wed, 2003-02-12 at 18:23, Serge Leblanc wrote:
> On Wed, Feb 12, 2003 at 11:36:35AM +0100, Giuseppe Castagna wrote:
> > Hello Serge,
> > 
> > I was asking myself exactly the same question. Do you want to extract
> > XML transformations that you specify in Coq? I'm *very* curious to know
> > why you chose CDuce as a target language (I'm not against it, on the
> > contrary!... FYI I'm one of the persons working on the definition of
> > CDuce). I see that the higher order functions of CDuce can be useful
> > for that, but it seems a little bit hard to compensate the absence of
> > polymorphic types (and I cannot promise you that we will come out with a
> > satisfactory definition in short time).
> 
> 
> My goal is to use Coq to specify and prove the compositions of
> transformations of documents XML and to extract from this specifycation a
> certified program.


I see, so your idea is that you want to build complex XML
transformations by composing simpler transformations that are certified.
In this way if you have the right composition operators you can use Coq
to certify the whole transformation. Yeah, I see the ideas that underlie
"Transmorpher" (Serge is one of the authors): you put the effort of Coq
specification to have a complete library of small building blocks and
you have a certification for the complex transformation for free. Nice!

So the key point for choosing CDuce is "higher order"

> 
> I chose CDuce for these innovating features: Typed, Functional, Static
> verification ... and it's well adapted to XML documents manipulation.

These characteristics are also those of XDuce (of course, since CDuce is
at the beggining an extension of XDuce). A point in favour of XDuce over
CDuce w.r.t. what you want to do is that the very persons of Caml (e.g.
Michel Mauny) are working on embedding XDuce in OCaml, and so this could
yield to a smoother migration for Coq extraction. Therefore although
XDuce is not higher order it could be an interesting candidate you
should take into account for Coq extraction.

---Beppe--- 


P.S. Hope that this discussion will not bother the coq-club members.

> 
> I do not think that the absence of polymorphic is a limitation for
> extraction. But integration of the polymorphise in CDuce will be a great
> improvement.
> 
> 
> On Wed, Feb 12, 2003 at 03:14:38PM +0100, Pierre Letouzey wrote:
> > 
> > PS: What about a meeting about this Coq->CDuse extraction ? I don't know 
> > where Serge is geographically located, but at least the database and
> > demons groups of LRI are not far away. And ENS Ulm isn't at the
> > antipodes...
> > 
> 
> I live near Grenoble and I can easely travel to Paris or Lyon.