Home page: Informatique
FlexDLL
MathématiquesLes textes présentés sont au format .dvi, .ps, ou .pdf. Si vous avez des problèmes pour lire les textes, ou si avez des suggestions ou des commentaires, n'hésitez pas à me contacter.
Ma page de mathématiques vous interessera peut-être aussi.
Thèse
Ma thèse porte sur la conception et l'implémentation du langage CDuce. Je l'ai soutenue le 13 décembre 2004.
Vous pouvez consulter mes publications ainsi que le site web de CDuce pour plus d'informations.
DEA
J'ai suivi le DEA de Paris 7, intitulé Programmation: sémantique, preuves et langages. J'ai effectué mon stage dans le laboratoire d'informatique de l'ENS, sous la direction de Giuseppe Castagna et Véronique Benzaken.
Le titre du mémoire est Types récursifs, combinaisons booléennes et fonctions surchargées: application au typage de XML. Je l'ai soutenu le 17 septembre 2001.
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.
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.
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.
Exposés pour des cours de DEA
Voici les transparents que j'ai utilisé pour présenter des articles, en guise d'examen pour certains cours de DEA.
- Typing Constraint Logic Programs. À propos de l' article de François Fages et Emmanuel Coquery. Pour le cours de Programmation par Contrainte.
- Classifying holes of arbitrary dimensions in partially ordered cubes. À propos de l'article de Stefan Sokolowski. Pour le cours de Sémantique Géométrique.
Stage de deuxième année
J'ai redigé les textes suivants lors d'un stage de quatre mois au AI Lab du MIT (septembre-decembre 1999).
- Exposé. Généralités sur les méthodes de déformation de variétés.
- Transparents. Sur l'article ci-dessus.
Divers
- Ordres bien fondés, beaux ordres, et extensions classiques. Une preuve assez rapide du théorème de Kruskal sur l'ordre plongement (et un lemme original ?).
- Plus petit point fixe, dérivation et stratégie. Un petit texte qui généralise la notion de dérivation (dans le sens "dérivation de typage") au cas non continu. Une dérivation est un objet qui prouve qu'un élément d'un treillis est plus petit que le plus petit point fixe d'une fonction croissante. On prouve la correction et la complétude de la notion, et on l'applique pour donner une caractérisation du plus petit point fixe en terme de jeu et de stratégie gagnante.
- Distance d'édition entre deux mots. Résolution du problème par programmation dynamique. Une implémentation en Caml-light.
- Arbre couvrant minimal. Les algorithmes de Prim et de Kruskal.
Home page: Informatique