The Coq mailing list

[Serge Leblanc <serge.leblanc AT wanadoo.fr>]

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 chose CDuce for these innovating features: Typed, Functional, Static
verification ... and it's well adapted to XML documents manipulation.

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.

-- 
Serge Leblanc
110 rue de charnècles
38340 Voreppe
tél: 06 23 22 55 58
GnuPG Key ID : 73791C2B
GnuPG Key fingerprint = 8817 E63A 82D4 EFE9 E28B  FDFE C9F6 6104 19A9 BFA6