This page contains Other pages: |
|
This site has been generated by CDuce . For a more detailed presentation of the script visit this page |
|
| Stages de Master Recherche d'Informatique | | Langage de mises a jour en CDuce | Responsables G. Castagna (L.I.E.N.S), V. Benzaken (L.R.I)
D. Colazzo (L.R.I).
Contexte
CDuce est un langage de programmation pour XML developpe conjointement par
l'equipe ``Langages'' du Laboratoire d'Informatique de l'ENS et l'equipe
``Bases de Donnees'' du LRI Orsay. Parmi ses caracteristiques principales
on peut citer, un systeme de types puissant (ordre superieur,
intersections, unions, negations, surcharge,...), l'integration des standards W3C
(XML, Unicode, namespaces, XML Schema, DTD, ...) un langage de
patterns tres expressif (expressions regulieres de types, capture de
sous-sequences d'elements non-consecutifs,...) et un runtime innovant (compilation
``just-in-time'' des patterns, automates d'arbres
``non-uniformes'',...).
Resume du travail souhaite
Dans un premier temps le stagiaire devra concevoir et developper la
definition d'un langage de mises a jours. Il devra donc en preciser sa syntaxe et sa semantique. Il devra definir son systeme de types en se basant sur le systeme de types de CDuce. Si le temps le permet les resultats devront etre implantes dans le langage CDuce.
Connaissances prealables attendues chez le stagiaire
Connaissance de la programmation fonctionnelle (OCaml), compilation, informatique theorque. La connaissance de theorie des types, programmation Web et de XML.
est un atout supplementaire.
References - Semantic subtyping . A. Frisch , G. Castagna , and V. Benzaken . in Proc of the
Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS'2002), pages 137-146,
Copenhagen, Denmark,22th-25th July.
(PS )
Retribution possible. Laboratoires - Laboratoire d'Informatique de l'Ecole Normale Superieure
- LRI, Universite de Paris XI.
Lieu du stage
LRI
|
| Specification et Preuve de Programmes CDuce. | Responsables V. Benzaken (L.R.I) G. Castagna (L.I.E.N.S) Ch. Paulin (L.R.I) D. Colazzo (L.R.I).
Contexte
CDuce est un langage de programmation pour XML developpe conjointement par
l'equipe ``Langages'' du Laboratoire d'Informatique de l'ENS et l'equipe
``Bases de Donnees'' du LRI Orsay. Parmi ses caracteristiques principales
on peut citer, un systeme de types puissant (ordre superieur,
intersections, unions, negations, surcharge,...), l'integration des standards W3C
(XML, Unicode, namespaces, XML Schema, DTD, ...) un langage de
patterns tres expressif (expressions regulieres de types, capture de
sous-sequences d'elements non-consecutifs,...) et un runtime innovant (compilation
``just-in-time'' des patterns, automates d'arbres
``non-uniformes'',...).
Travail demande
La construction de sites Web contenant de tres nombreuses pages rend
de plus en plus complexe voir impossible la verification de proprietes
sur ces pages. On peut vouloir garantir qu'un lien sur le site
correspond a une page existante, la coherence des donnees entre deux
pages distinctes, des proprietes sur les transformations de page
.
Lorsque les pages sont engendrees par programme, il est possible de
raisonner statiquement sur le code de celui-ci pour garantir la
correction finale du resultat.
L'objectif du stage est de mettre en place les bases d'un systeme de
specification et de verification pour CDuce.
Le systeme WHY (http://why.lri.fr/) propose une langage de
programmation et de specification generique permettant d'extraire des
proprietes suffisantes garantissant la correction du programme par
rapport à sa specification, ces proprietes pouvant ensuite être
demontree par differents outils de preuve automatique ou
interactifs.
Retribution possible. Laboratoires - Laboratoire d'Informatique de l'Ecole Normale Superieure
- LRI, Universite de Paris XI.
Lieu du stage
LRI
|
| Optimisation de requetes patterns au moyen de modules d'acces XML (XAMs) | Responsables V. Benzaken (L.R.I) I. Manolescu (INRIA) D. Colazzo (L.R.I).
Contexte
Le langage CQL est un langage de requete pour CDuce qui utilise comme
principale primitive d'extraction des patterns et comme mecanisme d'execution le pattern-matching. A ce jour seule des techniques d'optimisation en memoire centrale sont definies pour CQL. L'objectif est de proposer des techniques d'optimisation de requetes en gerant la memoire secondaire. Ceci se fera en utilisant des modules d'acces XML (XAM's).
Travail demande
Dans un premier temps, le stagiare devra se familiariser avec CQL et les XAM.
Ensuite, il devra proposer un moyen de generer des plans d'executions bases sur les XAM en analysant une requete CQL. Enfin, si le temp le permet il implantera cela au sein d'un prototype.
References - Uload: Choosing Right Storage
for your XML Application. A. Arion, V.Benzaken, I. Manolescu, and R. Vijay. Demonstration at the 31st International Conference on Very Large Databases VLDB 2005
- XML Access Modules: Towards Physical Data Independence in XML Databases. A. Arion, V.Benzaken, and I. Manolescu. In the Second International Workshop on XQuery Implementation, Experience and Perspective XIME-P 2005
(PDF)
- A Full Pattern-based Paradigm for XML Query Processing. V.Benzaken, G.Castagna, and C.Miachon. In the Seventh International Symposium on Practical Aspects of Declarative Languages PADL 2005
Retribution possible. Laboratoires - Projet Gemo INRIA - Futurs
- LRI, Universite de Paris XI.
Lieu du stage
LRI
|
| | Typage de requetes XQuery : précision et complexité | Responsables D.
Colazzo (L.R.I). V.
Benzaken (L.R.I). Contexte
XQuery est le langage de requete pour XML défini par le W3C, et est déjà
devenu un standard. Selon la définition du W3C, XQuery est doté d'un
système de types conforme à XML Schema et qui permet de détecter les
erreurs de type d'une requête, et de déterminer le type de son résultat.
La précision et la complexité de cette analyse de type n'ont pas encore
été étudiés de manière exhaustive. En autre le typage des opérateurs
XQuery de mis-à-jour et de navigation en arrière (en utilisant les axes
parent et ancestor) est un problème totalement ouvert actuellement.
Une premiere étude de ces aspects à été fait dans la thèse de doctorat
''Path Correctness for XML Queries: Characterization and Static Type
Checking'', par Dario Colazzo, qui montre comme augmenter la précision du
système de type de XQuery proposé par le W3C, en absence de mise à jour et
et de navigation en arrière. Toutefois, au présent, il manque encore une
étudie comparative entre le système proposé dans cette thèse et celui
proposé par le W3C. Le première objectif du stage est donc d'étudier
cette comparaison au niveau formel, alors que le deuxième est, si le temps
le permet, de définir et étudier un système de type pour les opérateurs
de navigation en arrière, et de mis à jour.
Travail demande Dans un premier temps, le stagière
devra se familiariser avec XQuery et sa sémantique; dans ce but il pourra
consulter la thèse mentionnée ci-dessus, des articles publiés dans des
conférences internationales, et enfin la documentation W3C disponible sur
le Web. Ensuite il devra conduire l'étude en identifiant des classes des
requêtes XQuery avec un niveau particulier de précision de typage et de
complexité de l'analyse de type. Enfin, si le temps le permet, il pourra
aussi étendre l'étudie aux problèmes de mise à jour et de navigation en
arrière.
References : -
Static analysis for path correctness of XML queries. Dario Colazzo , Giorgio Ghelli , Paolo Manghi , and Carlo Sartiani . A paraître dans Journal of Functional Programming
(pdf)
- Path Correctness for XML Queries: Characterization and Static
Type Checking
. Dario Colazzo . These de Doctorat(pdf)
Laboratoires - LRI, Universite de Paris XI.
Lieu du stage
LRI
|
| |
| Last update: 14 décembre 2005 |
| |