Vers une formalisation en Coq de la provenance de données

Véronique Benzaken (1) , Sarah Cohen-Boulakia (2) , Évelyne Contejean (1) , Chantal Keller (1) , Rébecca Zucchini (1, 3)

1 LRI - Laboratoire de Recherche en Informatique
2 BioInfo - LRI - Bioinformatique (LRI)
3 ENS Cachan - École normale supérieure - Cachan

Dans de multiples domaines scientifiques, de nombreuses données sont générées quotidiennement et doivent être analysées. Dans ces processus d’analyse, les données initiales sont combinées à d’autres jeux de données massifs. Pour garantir une interprétation correcte des résultats de ces analyses de données, il est crucial de pouvoir retracer la provenance des données produites à partir des données initiales. La communauté des bases de données a proposé un cadre formel unifiant de «semi-anneaux de provenance». L'objectif de cet article est de certifier a posteriori la correction d’une provenance. Pour ce faire, nous proposons une formalisation en Coq fondée sur le modèle de semi-anneaux de provenance pour des analyses de données exprimées en algèbre relationnelle. Nous introduisons ici notamment une preuve d'adéquation de cette provenance avec l'interprétation usuelle de l'algèbre relationnelle. Il s'agit d'une première étape vers la formalisation de langages centrés données avec des garanties fortes de provenance

Domaines: Informatique [cs]; Logique en informatique [cs.LO]

Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, Rébecca Zucchini. Vers une formalisation en Coq de la provenance de données. 31ème Journées Francophones des Langages Applicatifs, Jan 2020, Gruissan, France. pp.72-87. ⟨hal-03080066⟩