coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: G�rard Huet <Gerard.Huet AT inria.fr>
- To: Giuseppe Castagna <Giuseppe.Castagna AT ens.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.
- Date: Thu, 20 Feb 2003 18:40:26 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Build an Coq-CDuce extraction functionnality., Serge Leblanc
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Claudio Sacerdoti Coen
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Veronique Benzaken
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Giuseppe Castagna
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Pierre Letouzey
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Serge Leblanc
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Giuseppe Castagna
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Gérard Huet
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Serge Leblanc
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Giuseppe Castagna
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality., Pierre Letouzey
- Re: [Coq-Club] Build an Coq-CDuce extraction functionnality.,
Claudio Sacerdoti Coen
Archive powered by MhonArc 2.6.16.