Skip to content

GitLab

Commit 111149b6 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2003-03-16 17:53:51 by cvscast] Empty log message 

Original author: cvscast
Date: 2003-03-16 17:53:52+00:00
parent 3953a348
Hide whitespace changes
Inline Side-by-side
web/index.xml 0 → 100644
View file @ 111149b6
<?xml version="1.0" encoding="ISO-8859-1" standalone="yes"?>
<page>
<title>CDuce</title>
<banner>
<img title="CDuce" src="img/cduce_logo.jpg" width="400" height="206"
alt="CDuce"/>
</banner>
<!-- ********* Left panel ********* -->
<navig>
<toc/>
<box>
<p> CDuce ("seduce") is a new typed functional language with
innovative features: </p>
<ul>
<li> a rich <b>type algebra</b>, with recursive types and arbitrary
boolean combinations (union, intersection, complement); </li>
<li> a natural notion of <b>subtyping</b>, which allows to use a value
of a given type where a value of a supertype is expected; </li>
<li> <b>overloaded functions</b> with late binding (dynamic dispatch);
</li>
<li> a powerful <b>pattern matching</b> operation, with dynamic
dispatch ontypes and recursive patterns. </li>
</ul>
<p> Although CDuce is a general programming language, it features
several characteristics that make it adapted to XML documents
manipulation (transformation, extraction of information, creation of
documents).
<a href="http://www.w3.org/XML/">XML</a> is a syntax to
describe tree-like documents (aka semi-structured data), and XML
documents often come with a description of their type. The type is
expressed in a system like DTD, or
<a href="http://www.w3.org/XML/Schema">XML Schema</a>. </p>
<p> Our point of view and our guideline for the design of CDuce is
that a programming language for XML should take XML types into account
to allow: </p>
<ul>
<li> <b>static verifications</b> of properties for the applications
(for instance, ensuring that a transformation produces a document of
the expected type);</li>
<li> good <b>integration in a general purpose typed programming
language</b>;</li>
<li> static <b>optimizations</b> of applications and storage (knowing
the type of a document seems important to store and extract
information efficiently).</li>
</ul>
</box>
<box>
<p> <b>CDuce</b> is developped by the
<a href="http://www.di.ens.fr/~castagna/EQUIPE"><b>Languages</b></a>
group of ENS in Paris and the
<a href="http://www.lri.fr/bd"><b>Databases</b></a> group of LRI in
Orsay, two <a href="http://www.cnrs.fr">CNRS</a> labs.
</p>
</box>
<box>
<p> This page was automatically generated from an XML description of
the content by a CDuce program.
<img src="img/cducepower2.jpg" alt="Powered by CDuce"/></p>
</box>
<toc/>
</navig>
<!-- ********* Main panel ********* -->
<main>
<box title="Give it a try!" link="proto">
<section title="Online running prototype">
<p> The only available implementation of CDuce is an <a
href="cgi-bin/cduce">online prototype</a>. To get a feeling of CDuce,
you can try the examples and play with them, or have a look at this <a
href="memento.html">memento</a> which briefly explains the syntax of
the language. </p>
</section>
</box>
<box title="Papers" link="papers">
<section title="Language Description">
<ul>
<li>
<paper file="papers/cduce-wp.ps.gz">
<title>CDuce: a white paper</title>
<author>V. Benzaken</author>
<author>G. Castagna</author>
<author>A. Frisch</author>
<comment>
A preliminary and abriged version of this work was presented at the workshop
<i>PLAN-X: Programming Language Technologies for XML</i>
Pittsburgh PA, Oct. 2002.
</comment>
<abstract> <p> In this paper, we present the functional language CDuce,
discuss some design issues, and show its adequacy for working with
XML documents. Peculiar features of CDuce are a powerful pattern
matching, first class functions, overloaded functions, a very rich
type system (arrows, sequences, pairs, records, intersections,
unions, differences), precise type inference and a natural
interpretation of types as sets of values. We also discuss how to add
constructs for programming XML queries in a declarative (and, thus,
optimizable) way and finally sketch a dispatch algorithm to
demonstrate how static type information can be used in efficient
compilation schemas. </p> </abstract>
</paper>
</li>
</ul>
</section>
<section title="Theoretical foundations">
<ul>
<li>
<paper file="papers/lics02.ps.gz">
<title>Semantic subtyping</title>
<author>A. Frisch</author>
<author>G. Castagna</author>
<author>V. Benzaken</author>
<comment> In <i>LICS 2002</i>. </comment>
<abstract> <p> Usually subtyping relations are defined either
syntactically by a formal system or semantically by an interpretation
of types in an untyped denotational model. In this work we show how
to define a subtyping relation semantically, for a language whose
<i>operational</i> semantics is <i>driven by types</i>; we consider a
rich type algebra, with product, arrow, recursive, intersection,
union and complement types. Our approach is to "bootstrap" the
subtyping relation through a notion of set-theoretic model <i>of the
type algebra</i>. </p>
<p> The advantages of the semantic approach are manifold. Foremost we
get "for free" many properties (e.g., the transitivity of subtyping)
that, with axiomatized subtyping, would require tedious and error
prone proofs. Equally important is that the semantic approach allows
one to <i>derive</i> complete algorithms for the subtyping relation
or the propagation of types through patterns. As the subtyping
relation has a natural (inasmuch as semantic) interpretation, the
type system can give informative error messages when static
type-checking fails. Last but not least the approach has an immediate
impact in the definition <i>and the implementation</i> of languages
manipulating XML documents, as this was our original motivation.
</p> </abstract>
</paper>
</li>
<li>
<paper file="papers/itrs02.ps.gz">
<title>The Relevance of Semantic Subtyping</title>
<author>M. Dezani-Ciancaglini</author>
<author>A. Frisch</author>
<author>E. Giovannetti</author>
<author>Y. Motohama</author>
<comment>
In <i>Electronic Notes in Theoretical Computer Science 70 No.1 (2002)</i>.
</comment>
<abstract> <p> We compare Meyer and Routley's minimal relevant logic
B+ with the recent semantics-based approach to subtyping introduced
by Frisch, Castagna and Benzaken in the definition of a type system
with intersection and union. We show that - for the functional core
of the system - such notion of subtyping, which is defined in purely
set-theoretical terms, coincides with the relevant entailment of the
logic B+. </p> </abstract>
</paper>
</li>
<li>
<paper file="papers/dea.ps.gz">
<title>Types récursifs, combinaisons booléennes et fonctions
surchargées: application au typage de XML</title>
<author>A. Frisch</author>
<comment>In french. Mémoire du DEA « Programmation: Sémantique,
Preuves et Langages » (Paris VII) </comment>
<abstract> <p> Nous étudions un lambda-calcul typé avec une opération
de filtrage qui permet d'exprimer des fonctions
surchargées. L'algèbre de types a des types de base, les types
produit et flèche, les types récursifs, les combinaisons booléennes
finies arbitraires. Nous considérons une notion de sous-typage
sémantique, issue de l'interprétation des types comme ensembles de
valeurs du langage. </p>
<p> Les caractéristiques présentes dans le calcul et l'algèbre de
types sont motivées par l'utilisation du calcul comme un noyau pour
un langage adapté à la manipulation de documents XML. </p>
<p> Nous utilisons une approche sémantique pour étudier l'algèbre de
types, tout en conservant une preuve syntaxique de préservation du
typage par réduction. </p> </abstract>
</paper>
</li>
</ul>
</section>
<section title="Security">
<ul>
<li>
<paper file="papers/sec.ps.gz">
<title>Security analysis for XML transformations</title>
<author>M. Burelle</author>
<author>V. Benzaken</author>
<author>G. Castagna</author>
<comment> <a href="http://www.myths.eu.org">MyThS</a> technical
report. </comment>
<abstract> <p> In this article we give a formal definition of
information flows in the context of XML transformations and, more
generally, in the presence of type dependent computations. We
formalize a sound technique to detect XML document transformations
that may leak private or confidential information. By defining
security annotations and by relating various kind of analyses to
different query scenarios, we also establish a general framework for
checking middleware-located information flows. </p> </abstract>
</paper>
</li>
</ul>
</section>
</box>
<box title="Slides" link="slides">
<ul>
<li>
<slides file="slides/lri02.pdf">
<title>Semantic Subtyping</title>
<author>A. Frisch</author>
<author>G. Castagna</author>
<author>V. Benzaken</author>
<comment>Slides of a presentation given at LRI Database Group (2002-12)</comment>
</slides>
</li>
<li>
<slides file="slides/planx2002.pdf.gz">
<title>CDuce: a white paper</title>
<author>V. Benzaken</author>
<author>G. Castagna</author>
<author>A. Frisch</author>
<comment>Slides of the presentation given at the PLANX 2002 Workshop
in Pittsburgh (2002-09)</comment>
</slides>
</li>
<li>
<slides
file="ftp://ftp.ens.fr/pub/di/users/castagna/SLIDES/cduce-wp-slides.pdf.gz">
<title>CDuce: a white paper</title>
<author>V. Benzaken</author>
<author>G. Castagna</author>
<author>A. Frisch</author>
<comment>Slides of the presentation given at MyThS meeting in
Bertinoro (2002-12) </comment>
</slides>
</li>
<li>
<slides file="ftp://ftp.ens.fr/pub/di/users/castagna/SLIDES/cduce-sec.ps.gz">
<title>CDuce: document security</title>
<author>V. Benzaken</author>
<author>M. Burelle</author>
<author>G. Castagna</author>
<comment>Slides of the presentation given at FOSAD school (september
2002) </comment>
</slides>
</li>
</ul>
</box>
<box title="Related links" link="links">
<ul>
<li> <link url="http://xduce.sourceforge.net/" title="XDuce"> The
starting point of our work on semantic subtyping and CDuce was XDuce.
CDuce extends XDuce with first-class and late-bound overloaded
functions, and generalizes the boolean connectives (explicit union,
intersection, negation types). </link> </li>
<li> <link url="http://www.research.avayalabs.com/user/wadler/xml/"
title="XML: Some hyperlinks minus the hype"> By Philip Wadler. </link>
</li> </ul> </box>
<meta>
<p>
<a href="comeon.htm">
<img style="border:0;width:88px;height:31px"
src="img/cducepower3.png"
alt="Powered by CDuce"/>
</a>
<a href="http://validator.w3.org/check?uri=http%3A%2F%2Fwww.cduce.org%2Fcduce2.html">
<img style="border:0;width:88px;height:31px"
src="http://www.w3.org/Icons/valid-xhtml10"
alt="Valid XHTML 1.0!"/>
</a>
<a href="http://jigsaw.w3.org/css-validator/validator?uri=http://www.cduce.org/cduce2.html">
<img style="border:0;width:88px;height:31px"
src="http://jigsaw.w3.org/css-validator/images/vcss"
alt="Valid CSS!"/>
</a>
<a href="http://www.ens.fr">
<img style="border:0"
src="img//symbENSmio.gif"
alt="ENS" title="ENS"/>
</a>
<a href="http://www.u-psud.fr">
<img style="border:0"
src="img//symbP11mio.gif"
alt="Paris 11" title="Paris 11"/>
</a>
<a href="http://www.cnrs.fr">
<img style="border:0"
src="img//symbCNRSmio.gif"
alt="CNRS" title="CNRS"/>
</a>
</p>
<p>
<a href="mailto:Alain.Frisch@ens.fr">Mail the webmaster</a>
</p>
</meta>
</main>
</page>
web/site.cd
View file @ 111149b6
include "xhtml-strict.cd";;
include "xhtml-categ.cd";;
type Site = <site>[ <page {|input=String; output=String|}>[]* ];;
type Page = <page>[
<title>String
<banner>[InlineText*]
......@@ -98,14 +100,26 @@ let fun page2html (Page -> Xhtml)
]
];;
let page : Page = match load_xml "site.xml" with
| Page & p -> p
| _ -> raise "Invalid input document";;
let fun do_page((String,String) -> [])
(inf,outf) ->
let _ = print [ 'Loading ' !inf '... ' ] in
let page = match load_xml inf with
| Page & p -> p
| _ -> raise ("Invalid input document" @ inf) in
let _ = print [ 'Generating html ... ' ] in
let html : String =
[ '<?xml version="1.0" encoding="iso-8859-1"?>'
'<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"'
' "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">'
!(print_xml (page2html page)) ] in
let _ = print [ 'Saving to ' !outf '...\n' ] in
dump_to_file outf html;;
let out : String =
[ '<?xml version="1.0" encoding="iso-8859-1"?>'
'<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"'
' "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">'
!(print_xml (page2html page)) ];;
dump_to_file "index.html" out;;
let site =
let _ = print [ 'Loading site.xml ...\n' ] in
match load_xml "site.xml" with
| Site & <site>s ->
(transform s with <page input=inf; output=outf>[] ->
do_page(inf,outf))
| _ -> raise "Invalid site.xml";;
web/site.xml
View file @ 111149b6
<?xml version="1.0" encoding="ISO-8859-1" standalone="yes"?>
<page>
<title>CDuce</title>
<banner>
<img title="CDuce" src="img/cduce_logo.jpg" width="400" height="206"
alt="CDuce"/>
</banner>
<!-- ********* Left panel ********* -->
<navig>
<toc/>
<box>
<p> CDuce ("seduce") is a new typed functional language with
innovative features: </p>
<ul>
<li> a rich <b>type algebra</b>, with recursive types and arbitrary
boolean combinations (union, intersection, complement); </li>
<li> a natural notion of <b>subtyping</b>, which allows to use a value
of a given type where a value of a supertype is expected; </li>
<li> <b>overloaded functions</b> with late binding (dynamic dispatch);
</li>
<li> a powerful <b>pattern matching</b> operation, with dynamic
dispatch ontypes and recursive patterns. </li>
</ul>
<p> Although CDuce is a general programming language, it features
several characteristics that make it adapted to XML documents
manipulation (transformation, extraction of information, creation of
documents).
<a href="http://www.w3.org/XML/">XML</a> is a syntax to
describe tree-like documents (aka semi-structured data), and XML
documents often come with a description of their type. The type is
expressed in a system like DTD, or
<a href="http://www.w3.org/XML/Schema">XML Schema</a>. </p>
<p> Our point of view and our guideline for the design of CDuce is
that a programming language for XML should take XML types into account
to allow: </p>
<ul>
<li> <b>static verifications</b> of properties for the applications
(for instance, ensuring that a transformation produces a document of
the expected type);</li>
<li> good <b>integration in a general purpose typed programming
language</b>;</li>
<li> static <b>optimizations</b> of applications and storage (knowing
the type of a document seems important to store and extract
information efficiently).</li>
</ul>
</box>
<box>
<p> <b>CDuce</b> is developped by the
<a href="http://www.di.ens.fr/~castagna/EQUIPE"><b>Languages</b></a>
group of ENS in Paris and the
<a href="http://www.lri.fr/bd"><b>Databases</b></a> group of LRI in
Orsay, two <a href="http://www.cnrs.fr">CNRS</a> labs.
</p>
</box>
<box>
<p> This page was automatically generated from an XML description of
the content by a CDuce program.
<img src="img/cducepower2.jpg" alt="Powered by CDuce"/></p>
</box>
<toc/>
</navig>
<!-- ********* Main panel ********* -->
<main>
<box title="Give it a try!" link="proto">
<section title="Online running prototype">
<p> The only available implementation of CDuce is an <a
href="cgi-bin/cduce">online prototype</a>. To get a feeling of CDuce,
you can try the examples and play with them, or have a look at this <a
href="memento.html">memento</a> which briefly explains the syntax of
the language. </p>
</section>
</box>
<box title="Papers" link="papers">
<section title="Language Description">
<ul>
<li>
<paper file="papers/cduce-wp.ps.gz">
<title>CDuce: a white paper</title>
<author>V. Benzaken</author>
<author>G. Castagna</author>
<author>A. Frisch</author>
<comment>
A preliminary and abriged version of this work was presented at the workshop
<i>PLAN-X: Programming Language Technologies for XML</i>
Pittsburgh PA, Oct. 2002.
</comment>
<abstract> <p> In this paper, we present the functional language CDuce,
discuss some design issues, and show its adequacy for working with
XML documents. Peculiar features of CDuce are a powerful pattern
matching, first class functions, overloaded functions, a very rich
type system (arrows, sequences, pairs, records, intersections,
unions, differences), precise type inference and a natural
interpretation of types as sets of values. We also discuss how to add
constructs for programming XML queries in a declarative (and, thus,
optimizable) way and finally sketch a dispatch algorithm to
demonstrate how static type information can be used in efficient
compilation schemas. </p> </abstract>
</paper>
</li>
</ul>
</section>
<section title="Theoretical foundations">
<ul>
<li>
<paper file="papers/lics02.ps.gz">
<title>Semantic subtyping</title>
<author>A. Frisch</author>
<author>G. Castagna</author>
<author>V. Benzaken</author>
<comment> In <i>LICS 2002</i>. </comment>
<abstract> <p> Usually subtyping relations are defined either
syntactically by a formal system or semantically by an interpretation
of types in an untyped denotational model. In this work we show how
to define a subtyping relation semantically, for a language whose
<i>operational</i> semantics is <i>driven by types</i>; we consider a
rich type algebra, with product, arrow, recursive, intersection,
union and complement types. Our approach is to "bootstrap" the
subtyping relation through a notion of set-theoretic model <i>of the
type algebra</i>. </p>
<p> The advantages of the semantic approach are manifold. Foremost we
get "for free" many properties (e.g., the transitivity of subtyping)
that, with axiomatized subtyping, would require tedious and error
prone proofs. Equally important is that the semantic approach allows
one to <i>derive</i> complete algorithms for the subtyping relation
or the propagation of types through patterns. As the subtyping
relation has a natural (inasmuch as semantic) interpretation, the
type system can give informative error messages when static
type-checking fails. Last but not least the approach has an immediate
impact in the definition <i>and the implementation</i> of languages
manipulating XML documents, as this was our original motivation.
</p> </abstract>
</paper>
</li>
<li>
<paper file="papers/itrs02.ps.gz">
<title>The Relevance of Semantic Subtyping</title>
<author>M. Dezani-Ciancaglini</author>
<author>A. Frisch</author>
<author>E. Giovannetti</author>
<author>Y. Motohama</author>
<comment>
In <i>Electronic Notes in Theoretical Computer Science 70 No.1 (2002)</i>.
</comment>
<abstract> <p> We compare Meyer and Routley's minimal relevant logic
B+ with the recent semantics-based approach to subtyping introduced
by Frisch, Castagna and Benzaken in the definition of a type system
with intersection and union. We show that - for the functional core
of the system - such notion of subtyping, which is defined in purely
set-theoretical terms, coincides with the relevant entailment of the
logic B+. </p> </abstract>
</paper>
</li>
<li>
<paper file="papers/dea.ps.gz">
<title>Types récursifs, combinaisons booléennes et fonctions
surchargées: application au typage de XML</title>
<author>A. Frisch</author>
<comment>In french. Mémoire du DEA « Programmation: Sémantique,
Preuves et Langages » (Paris VII) </comment>
<abstract> <p> Nous étudions un lambda-calcul typé avec une opération
de filtrage qui permet d'exprimer des fonctions
surchargées. L'algèbre de types a des types de base, les types
produit et flèche, les types récursifs, les combinaisons booléennes
finies arbitraires. Nous considérons une notion de sous-typage
sémantique, issue de l'interprétation des types comme ensembles de
valeurs du langage. </p>
<p> Les caractéristiques présentes dans le calcul et l'algèbre de
types sont motivées par l'utilisation du calcul comme un noyau pour
un langage adapté à la manipulation de documents XML. </p>
<p> Nous utilisons une approche sémantique pour étudier l'algèbre de
types, tout en conservant une preuve syntaxique de préservation du
typage par réduction. </p> </abstract>
</paper>
</li>
</ul>
</section>
<section title="Security">
<ul>
<li>
<paper file="papers/sec.ps.gz">
<title>Security analysis for XML transformations</title>
<author>M. Burelle</author>
<author>V. Benzaken</author>
<author>G. Castagna</author>
<comment> <a href="http://www.myths.eu.org">MyThS</a> technical
report. </comment>
<abstract> <p> In this article we give a formal definition of
information flows in the context of XML transformations and, more
generally, in the presence of type dependent computations. We
formalize a sound technique to detect XML document transformations
that may leak private or confidential information. By defining
security annotations and by relating various kind of analyses to
different query scenarios, we also establish a general framework for
checking middleware-located information flows. </p> </abstract>
</paper>
</li>
</ul>
</section>
</box>
<box title="Slides" link="slides">
<ul>
<li>
<slides file="slides/lri02.pdf">
<title>Semantic Subtyping</title>
<author>A. Frisch</author>
<author>G. Castagna</author>
<author>V. Benzaken</author>
<comment>Slides of a presentation given at LRI Database Group (2002-12)</comment>
</slides>
</li>
<li>
<slides file="slides/planx2002.pdf.gz">
<title>CDuce: a white paper</title>
<author>V. Benzaken</author>
<author>G. Castagna</author>
<author>A. Frisch</author>
<comment>Slides of the presentation given at the PLANX 2002 Workshop
in Pittsburgh (2002-09)</comment>
</slides>