The Coq mailing list

[G�rard Huet <Gerard.Huet AT inria.fr>]

Le mercredi, 19 fév 2003, à 19:41 Europe/Paris, Giuseppe Castagna a 
écrit :
...
> 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.

Actually, I think this discussion is extremely interesting, because 
there is a very
important interaction between XML and its various type frameworks (DTD, 
Schemas, etc),
ML/Ocaml and its double system of types/functors, and TypeTheory/Coq 
with rich
inductive/coinductive types and program extraction.
One common concern for instance is complexity of type 
computation/inference, in the
presence of interacting features and possible type equations. One may 
view XML typing
as type checking modulo some regular expression equivalence, and such a 
feature, when
fully undrerstood, may be itself a good candidate for enrichment of the 
type theory of
Coq, in order to have some kind of overloading of logical expressions 
schemas with
regularities. In much the same way that the CCC isomorphisms type 
equivalences which
Roberto di Cosmo studied for locating functions in ML libraries could 
be put to use
in Coq for precisely the same problem - logical organisation of 
mathematical libraries.
Cheers
Gérard