The Coq mailing list

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

On Wed, Feb 19, 2003 at 07:41:11PM +0100, Giuseppe Castagna wrote:
> 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!

Yes, and Coq seems to be a good tool for the analysis 
of the compositions of transformation, with an aim of infer of knowledge.

NB: I am not exactly a author of Transmorpher but I contributed to his
emergence via the management of the Fluxmedia start-up. Fluxmedia and
EXMO Inria team carried out Transmorpher in partnership. Infortunately,
following economic difficulty Fluxmedia had to stop its activity but 
Transmorpher is currently under active development coming from EXMO.


http://exmo.inrialpes.fr/software/transmorpher/PR1.html


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

Yes, also.


> > 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.

I don't know if embedding XDuce in Ocaml is not higher order although
XDuce is not of a higher order. I have not had of news of this project
for several months ago and I don't know its status, exactly features and
availability.

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