Bibliothèque certifiée en Coq pour la provenance des données
par Rébecca Zucchini
Mardi 4 juillet 2023 à 14h
ENS Paris-Saclay, salle 1Z14
Résumé : La présente thèse se situe à l'intersection des méthodes formelles et des bases de données, et s'intéresse à la formalisation de la provenance des données à l'aide de l'assistant de preuve Coq. L'étude de la provenance des données, qui permet de retracer leur origine et leur historique, est essentielle pour assurer la qualité des données, éviter les interprétations erronées et favoriser la transparence dans le traitement des données. La thèse propose ainsi la formalisation de deux types de provenance des données couramment utilisés, la How-provenance et la Where-provenance. Cette formalisation a permis de comparer leur sémantique, mettant en évidence leurs différences et leurs complémentarités. En outre, elle a conduit à la proposition d'une structure algébrique et d'une sémantique unificatrice pour ces deux types de provenance.
Abstract: This thesis is about the formalization of data provenance using the Coq proof assistant, at the intersection of formal methods and database communities. It explores the importance of data provenance, which tracks the origin and history of data, in addressing issues such as poor data quality, incorrect interpretations, and lack of transparency in data processing. The thesis proposes formalizations of two commonly used types of data provenance, How-provenance and Where-provenance. Formalizing both types of provenance allowed us to compare their semantics, highlighting their differences and complementarities. Additionally, the formalization of these two types of provenance led to the proposal of an algebraic structure that provides a unifying semantics.
Directrice de thèse et encadrantes :
- Mme Véronique BENZAKEN, Professeure des universités, LMF, Universite Paris Saclay - Directrice de thèse
- Mme Sarah COHEN-BOULAKIA, Professeure des universités, LISN, Universite Paris Saclay - Co-encadrante de thèse
- Mme Chantal KELLER, Maîtresse de conférences, LMF, Universite Paris Saclay - Co-encadrante de thèse
Jury:
- Mme Catherine DUBOIS, Professeure des universités, ENSIIE, Université Paris Saclay - Examinateur
- Mme Assia MAHBOUBI, Directrice de recherche, Inria Nantes/ LS2N, Université de Rennes - Examinateur
- M. Yves BERTOT, Directeur de recherche, Inria Sophia Antipolis, Université Côte d'Azur - Rapporteur
- M. Pierre SENELLART, Professeur des universités, École normale supérieure, Université Paris Sciences et Lettres - Rapporteur
- M. Nicolas THIERY, Professeur des universités, LISN, Université Paris Saclay - Examinateur