Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Formalisation en Coq de Bases de Données Relationnelles et Déductives - et Mécanisation de Datalog
Début le 01/10/2012
Direction : BENZAKEN, Véronique
[CONTEJEAN Evelyne]
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI-Proval
Soutenue le 02/12/2016 devant le jury composé de :
Directrices de thèse :
- Mme. Véronique Benzaken, Professeur, Université Paris-Sud, LRI
- Mme. Évelyne Contejean, Chargée de Recherche HDR, CNRS, LRI
Rapporteurs :
- Mme. Sandrine Blazy, Professeur, Université de Rennes 1, INRIA Rennes - Bretagne Atlantique
- M. Mohand-Saïd Hacid, Professeur, Université Claude Bernard Lyon 1, LIRIS
Examinateurs :
- Mme. Sarah Cohen-Boulakia, Maître de Conférences HDR, Université Paris-Sud, LRI
- M. Michaël Rusinowitch, Directeur de Recherche, Université Henri Poincaré Nancy 1, LORIA-INRIA Lorraine
Activités de recherche :
- Formalisation de langages (de spécification et de programmation) dans les assistants de preuve
- Langages et systèmes centrés données
Résumé :
Cette thèse présente une formalisation en Coq des langages et des algorithmes fondamentaux portant sur les bases de données. Cela fourni des spécifications formelles issues des deux approches différentes pour la définition des modèles de données: une basée sur l’algèbre et l'autre basée sur la logique.
A ce titre, une première contribution de cette thèse est le développement d'une bibliothèque Coq pour le modèle relationnel. Celui-ci contient des modélisations de l’algèbre relationnelle et des requêtes conjonctives. Il contient aussi une mécanisation des contraintes d'intégrité et de leurs procédures d'inférence. Nous modélisons deux types des dépendances, qui sont parmi les plus courantes: les dépendances fonctionnelles et les dépendances multivaluées, ainsi que leurs axiomatisations correspondants. Nous prouvons formellement la correction de leurs algorithmes d'inférence et, pour le cas de dépendances fonctionnelles, aussi la complétude. Ces types de dépendances sont des instances de dépendances générales : les dépendances génératrices d'égalité et, respectivement, les dépendances génératrices de tuples. Nous modélisons les dépendances générales et leur procédure d'inférence, c'est-à-dire, "le chase", pour lequel nous établissons la correction. Enfin, on prouve formellement les théorèmes principaux des bases de données, c'est-à-dire, les équivalences algébriques, le théorème de l'homomorphisme et la minimisation des requêtes conjonctives.
Une deuxième contribution consiste dans le développement d'une bibliothèque Coq/ssreflect pour la programmation logique, restreinte au cas du Datalog. Dans le cadre de ce travail, nous donnons la première mécanisation d'un moteur Datalog standard, ainsi que son extension avec la négation. La bibliothèque comprend une formalisation de leur sémantique en théorie des modèles ainsi que de leur sémantique par point fixe, implémentée par une procédure d'évaluation stratifiée. La bibliothèque est complétée par les preuves de correction, de terminaison et de complétude correspondantes. Dans ce contexte, nous construisons aussi un cadre préliminaire pour raisonner sur les programmes stratifiés. Cette plateforme ouvre la voie à la certification d'applications centrées données.
