Aujourd'hui, les contenus et les applications Web sont devenus la principale interface pour effectuer toutes sortes de tâches de la vie quotidienne comme déclarer et payer les impôts, réserver des billets d'avion ou de train, planifier des vacances, effectuer des achats, gérer les comptes bancaires, etc. En conséquence, il devient de plus en plus important d'étudier leurs fondements, d'améliorer leurs capacités, de faciliter leur conception, de vérifier leur fonctionnement, de les optimiser automatiquement et les rendre plus souples et adaptables aux usages et aux différentes plateformes. Dans ce document, nous décrivons d'abord mes activités professionnelles, concernant les années 1998 à 2012. La première partie de ce document contient un résumé de mes activités de recherche, d'encadrement, d'enseignement et charges administrative et collective, ainsi qu'un résumé de mes principaux résultats scientifiques. Dans le reste du document, nous introduisons une logique de raisonnement sur les arbres finis, une procédure de décision correcte et complète pour vérifier la satisfaisabilité d'une formule de la logique ainsi que d'une mise en œuvre efficace en pratique. La logique est une variante du mu-calcul adaptée aux arbres finis et équipée avec des modalités arrières et des nominaux. Ensuite, nous considérons le problème de l'évolution des schémas XML. Dans le contexte en constante évolution du Web, les schémas XML changent continuellement afin de faire face à l'évolution naturelle des entités qu'ils décrivent. Les modifications de schémas peuvent avoir des conséquences importantes dans la mesure où les documents existants peuvent devenir invalides et la programmes les manipulant incorrectes. Nous proposons un cadre unificateur pour déterminer les effets de l'évolution des schémas XML à la fois sur la validité des documents et des requêtes contenues dans ces programmes. Dans la dernière partie du document, nous considérons une algèbre de type équipée de la récursivité, du produit cartésien, des fonctions, de l'intersection, de l'union, et du complément ainsi que des variables de type et une quantification universelle implicite sur ces variables. Nous considérons la relation de sous-typage récemment définie par Castagna et Xu sur des expressions de cette algèbre de type et montrons que le sous-typage peut être décidé avec une complexité EXPTIME et implémenté efficacement en pratique clôturant ainsi à une question ouverte dans la littérature.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00872752 |
| Date | 23 April 2013 |
| Creators | Layaïda, Nabil |
| Publisher | Université de Grenoble |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | habilitation ࠤiriger des recherches |
Page generated in 0.0051 seconds