Commit 8513e665 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2002-12-11 20:25:32 by cvscast] Empty log message

Original author: cvscast
Date: 2002-12-11 20:25:33+00:00
parent 2f907fda
body {
background: #BBDDFF;
color: #000000;
margin: 1ex 0 1ex 0;
padding: 0;
}
a:link:hover, a:visited:hover {
text-decoration: none;
background: #FFFFD0;
color: #FF0000;
}
h1 {
color: #FF0000;
text-align: center;
font: bold 200% helvetica;
margin: 0ex 0em 0ex 0em;
padding: 0ex;
}
h2 {
background: #FFF0F0;
color: #0000FF;
font: bold 102% helvetica;
padding: 0.5ex 0 0.5ex 1em;
margin: 0 0 0 0;
}
h3 {
font: bold 60% sans-serif;
padding: 0 0 0 2em;
margin: 0 0 0 0;
}
h4 {
font: bold 100% helvetica;
color: #008000;
padding: 0 0 0 1em;
margin: 1em 0 0 0;
}
p {
text-align: justify;
margin: 1ex 1em 0 1em;
}
div.abstract {
font: bold 80% helvetica;
margin: 1ex 1em 1ex 1em;
padding: 1ex 1em 1ex 1em;
background: #F0F0F0;
}
div.abstract p {
font: 100% sans-serif;
}
#Sidelog {
position: absolute;
top: 10px;
left: 10px;
width: 170px;
background-color: #ffcd72;
border: 1px dashed black;
padding: 5px 5px 0px 5px;
font-size:11px;
font-family: arial, helvetica, sans-serif;
color: black;
}
#Content {
margin:10px 1em 10px 205px;
padding:10px 20px 10px 20px;
color:black;
background-color:#fccead;
border:1px solid black;
}
.box {
background: #FFFFFF;
border: solid 2px #000000;
margin: 2ex 1em 1em 1em;
padding: 0ex 0ex 0.5em 0ex;
}
div.title {
background: #FFFFFF;
border: solid 2px #000000;
margin:10px 1em 10px 205px;
padding: 0ex 0ex 0ex 0ex;
}
div.meta {
background: #E0E0E0;
margin: 4ex 0.5em 0 0.5em;
border: solid 1px #B0B0B0;
padding: 0.5ex;
font-size: 80%;
font-family: sans-serif;
}
@media screen {
body {
background: #fcb333;
}
}
<?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="cduce2.css" type="text/css"/>
<title>CDuce</title>
</head>
<body>
<banner title="CDuce" subtitle="Page last modified on 2002-12-05"/>
<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>
</div>
<div id="Content">
<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" />
</div>
</div>
</body>
</html>
type XML_elem = <(_)>XML;;
type XML = [ (XML_elem | Char)* ];;
let fun banner (title : Any, subtitle : Any) : XML =
[<div class="title">[
!(match title with t & XML \ [] -> [<h1>t] | _ -> [])
!(match subtitle with t & XML \ [] -> [<h3>t] | _ -> [])
]];;
let fun box (title : Any, subtitle : Any, name : Any, content : XML) : XML =
[<div class="box">[
!(match name with String \ [] -> [<a name=name>[]] | _ -> [])
!(match title with t & XML \ [] -> [<h2>t] | _ -> [])
!(match subtitle with t & XML \ [] -> [<h3>t] | _ -> [])
!content
]];;
let fun convert (XML_elem | Char | XML -> XML)
| <box ({ title=t }
& ({ subtitle=st } | (st := `nil))
& ({ link=name } | (name := `nil)) )>x ->
box (t,st,name,convert x)
| <banner ({ title=t } & ({ subtitle=st } | (st := `nil)))>x ->
banner (t,st)
| <(tag) (attr)>x -> [<(tag) (attr)>(convert x)]
| c & Char -> [c]
| seq -> transform seq with x -> convert x;;
let src =
match [ (load_xml "index2.xml") ] with
| XML & x -> x
| _ -> raise ("Invalid input ...");;
let conv : XML = convert src;;
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">' ]
@
(transform convert src with x -> print_xml x);;
dump_to_file "index2.html" out;;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment