Commit 0f1bf089 authored by Pietro Abate's avatar Pietro Abate
Browse files

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

Original author: cvscast
Date: 2003-03-16 17:35:53+00:00
parent a514da8a
<?xml version="1.0" standalone="yes" encoding="iso8859-1"?>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"/>
<link rel="stylesheet" href="cduce.css" type="text/css"/>
<title>CDuce</title>
</head>
<body>
<banner title="CDuce" subtitle="Page last modified on 2002-12-05"/>
<box title="">
<ul>
<li><a href="#proto">Give it a try !</a></li>
<li><a href="#papers">Papers</a></li>
<li><a href="#slides">Slides</a></li>
<li><a href="#links">Related links</a></li>
</ul>
</box>
<box title="">
<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 on types 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 title="Give it a try!" subtitle="Online running prototype"
link="proto">
<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>
</box>
<box title="Papers" subtitle="" link="papers">
<h4> Language Description</h4>
<ul>
<li>
<b>CDuce: a white paper</b>.
V. Benzaken, G. Castagna, and A. Frisch.
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.
<a href="papers/cduce-wp.ps.gz">(download ps.gz)</a>
<div class="abstract">
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>
</div>
</li></ul>
<h4>Theoretical foundations</h4>
<ul>
<li>
<b>Semantic subtyping</b>;
A. Frisch, G. Castagna, V. Benzaken. In <i>LICS 2002</i>.
<a href="papers/lics02.ps.gz">(download ps.gz)</a>
<div class="abstract">
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>
</div>
</li>
<li>
<b>Semantic subtyping, extended
version</b>. Soon available.</li>
<li>
<b>The Relevance of Semantic Subtyping</b>;
M. Dezani-Ciancaglini, A. Frisch, E. Giovannetti, Y. Motohama.
In <i>Electronic Notes in Theoretical Computer Science 70 No.1 (2002)</i>.
<a href="papers/itrs02.ps.gz">(download ps.gz)</a>
<a href="papers/itrs02.pdf">(download pdf)</a>
<div class="abstract">
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>
</div>
</li>
<li>
(In french) <b>Types récursifs,
combinaisons booléennes et fonctions surchargées: application
au typage de XML</b> (rapport de DEA); Alain Frisch.
<a href="papers/dea.ps.gz">
(download ps.gz)</a>
<div class="abstract">
Resumé:
<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>
</div>
</li>
</ul>
</box>
<box title="Slides" link="slides">
<ul>
<li>
<b>Semantic Subtyping</b>.
A. Frisch, G. Castagna, and V. Benzaken.
Slides of a presentation given at LRI Database Group (2002-12)
<a href="slides/lri02.pdf">(download pdf)</a></li>
<li>
<b>CDuce: a white paper</b>.
V. Benzaken, G. Castagna, and A. Frisch.
Slides of the presentation given at the PLANX 2002 Workshop in Pittsburgh (2002-09)
<a href="slides/planx2002.pdf.gz">(download pdf.gz)</a></li>
<li>
<b>CDuce: a white paper</b>.
V. Benzaken, G. Castagna, and A. Frisch.
Slides of the presentation given at MyThS meeting in Bertinoro (2002-12)
<a href="ftp://ftp.ens.fr/pub/di/users/castagna/SLIDES/cduce-wp-slides.ps.gz">(download
ps.gz)</a></li>
<li>
<b>CDuce: document security</b>.
V. Benzaken, M. Burelle, G. Castagna.
Slides of the presentation given at FOSAD school (september 2002)
</li>
</ul>
</box>
<box title="Related links" link="links">
<ul>
<li>
<b>XDuce</b>
The starting point of our
work on semantic subtyping and CDuce was <a href="http://xduce.sourceforge.net/">XDuce</a>.
CDuce extends XDuce with first-class and late-bound overloaded functions,
and generalizes the boolean connectives (explicit union, intersection,
negation types).
</li>
<li>
<a href="http://www.research.avayalabs.com/user/wadler/xml/">XML:
Some hyperlinks minus the hype</a> by Philip Wadler.</li>
</ul>
</box>
<div class="meta">
<a href="mailto:Alain.Frisch@ens.fr">Mail the webmaster</a>
<br/>
<img src="img/cducepower2.jpg"
alt="Powered by CDuce"/>
<img src="http://www.w3.org/Icons/valid-xhtml10"
alt="Valid XHTML 1.0!" height="31" width="88" />
<img style="border:0;width:88px;height:31px"
src="http://jigsaw.w3.org/css-validator/images/vcss"
alt="Valid CSS!">
</div>
</body>
</html>
<?xml version="1.0" encoding="iso8859-1" standalone="yes"?>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"/>
<php>
<![CDATA[
$browser = getenv("HTTP_USER_AGENT");
if (preg_match("/MSIE/i", "$browser")) {
$css = "<link rel=\"stylesheet\" href=\"cduce2.css\" type=\"text/css\">";
} elseif (preg_match("/Mozilla/i", "$browser")) {
$css = "<blink>For better presentation use a more recent version of your browser, such as Netscape 6 or Mozilla</blink>";
} if (preg_match("/Mozilla\/5.0/i", "$browser")) {
$css = "<link rel=\"stylesheet\" href=\"cduce2.css\" type=\"text/css\">";
} elseif (preg_match("/opera/i", "$browser")) {
$css = "<link rel=\"stylesheet\" href=\"cduceOpera.css\" type=\"text/css\">";
}
echo "$css";
]]>
</php>
<title>CDuce</title>
</head>
<body>
<banner title="CDuce" subtitle="Page last modified on 2002-12-05" src="img/cduce_logo.jpg" style="width: 400px; height: 206px;"/>
<div id="Sidelog">
<box title="">
<ul>
<li><a href="#proto">Give it a try !</a></li>
<li><a href="#papers">Papers</a></li>
<li><a href="#slides">Slides</a></li>
<li><a href="#links">Related links</a></li>
</ul>
</box>
<box title="">
<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 on types 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 title="">
<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
<center>
<img style="border:0;width:45px"
src="img//LogoCNRSMoyen.gif"
alt="CNRS"/>
</center>
</box>
<box title="">
This page was automatically generated from an XML description of the content by
a CDuce program
<p/>
<?php
$browser = getenv("HTTP_USER_AGENT");
if (preg_match("/Mozilla/i", "$browser")) {
if (preg_match("/Mozilla\/5.0/i", "$browser")) {
echo "<img src=\"img/cducepower2.jpg\" alt=\"Powered by CDuce\"/>"; } }
?>
</box>
</div>
<div id="Content">
<box title="Give it a try!" subtitle=""
link="proto">
<h4>Online running prototype</h4>
<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>
</box>
<box title="Papers" subtitle="" link="papers">
<h4> Language Description</h4>
<ul>
<li>
<b>CDuce: a white paper</b>.
V. Benzaken, G. Castagna, and A. Frisch.
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.
<a href="papers/cduce-wp.ps.gz">(download ps.gz)</a>
<div class="abstract">
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>
</div>
</li></ul>
<h4>Theoretical foundations</h4>
<ul>
<li>
<b>Semantic subtyping</b>;
A. Frisch, G. Castagna, V. Benzaken. In <i>LICS 2002</i>.
<a href="papers/lics02.ps.gz">(download ps.gz)</a>
<div class="abstract">
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>
</div>
</li>
<li>
<b>Semantic subtyping, extended
version</b>. Soon available.</li>
<p/>
<li>
<b>The Relevance of Semantic Subtyping</b>;
M. Dezani-Ciancaglini, A. Frisch, E. Giovannetti, Y. Motohama.
In <i>Electronic Notes in Theoretical Computer Science 70 No.1 (2002)</i>.
<a href="papers/itrs02.ps.gz">(download ps.gz)</a>
<a href="papers/itrs02.pdf">(download pdf)</a>
<div class="abstract">
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>
</div>
</li>
<li>
(In french) <b>Types récursifs,
combinaisons booléennes et fonctions surchargées: application
au typage de XML</b> (rapport de DEA); Alain Frisch.
<a href="papers/dea.ps.gz">
(download ps.gz)</a>
<div class="abstract">
Resumé:
<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>
</div>
</li>
</ul>
<h4>Security</h4>
<ul>
<li>
<b>Security analysis for XML transformations</b>;
M. Burelle, V. Benzaken, G. Castagna. <a href="http://www.myths.eu.org">MyThS</a> technical report.
<a href="papers/sec.ps.gz">(download ps.gz)</a>
<div class="abstract">
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>
</div>
</li>
</ul>
</box>
<box title="Slides" link="slides">
<ul>
<li>
<b>Semantic Subtyping</b>.
A. Frisch, G. Castagna, and V. Benzaken.
Slides of a presentation given at LRI Database Group (2002-12)
<a href="slides/lri02.pdf">(download pdf)</a></li>
<li>
<b>CDuce: a white paper</b>.
V. Benzaken, G. Castagna, and A. Frisch.
Slides of the presentation given at the PLANX 2002 Workshop in Pittsburgh (2002-09)
<a href="slides/planx2002.pdf.gz">(download pdf.gz)</a></li>
<li>
<b>CDuce: a white paper</b>.
V. Benzaken, G. Castagna, and A. Frisch.
Slides of the presentation given at MyThS meeting in Bertinoro (2002-12)
<a href="ftp://ftp.ens.fr/pub/di/users/castagna/SLIDES/cduce-wp-slides.pdf.gz">(download
ps.gz)</a></li>
<li>
<b>CDuce: document security</b>.
V. Benzaken, M. Burelle, G. Castagna.
Slides of the presentation given at FOSAD school (september 2002)
<a href="ftp://ftp.ens.fr/pub/di/users/castagna/SLIDES/cduce-sec.ps.gz">(download
ps.gz)</a></li>
</ul>
</box>
<box title="Related links" link="links">
<ul>
<li>
<b>XDuce</b>
The starting point of our
work on semantic subtyping and CDuce was <a href="http://xduce.sourceforge.net/">XDuce</a>.
CDuce extends XDuce with first-class and late-bound overloaded functions,
and generalizes the boolean connectives (explicit union, intersection,
negation types).
</li>
<li>
<a href="http://www.research.avayalabs.com/user/wadler/xml/">XML:
Some hyperlinks minus the hype</a> by Philip Wadler.</li>
</ul>
</box>
<div class="meta">
<table>
<tr>
<td>
<a href="mailto:Alain.Frisch@ens.fr">Mail the webmaster</a>
<p/>
<br/>
<?php
$browser = getenv("HTTP_USER_AGENT");
if (preg_match("/Mozilla/i", "$browser")) {
if (preg_match("/Mozilla\/5.0/i", "$browser"))
{
?><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>
</td>
<td><a href="http://www.ens.fr">
<img style="border:0"
src="img//symbENSmio.gif"
alt="ENS" title="ENS"/></a></td>
<td> </td>
<td><a href="http://www.u-psud.fr">
<img style="border:0"
src="img//symbP11mio.gif"