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

International audience ; 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 initialessont combinées à d’autres jeux de données massifs. Pour garantir une interprétation correctedes résultats de ces analyses de données, il est crucial de pouvoir retracer la provenance desdonnées produites à partir des données initiales. La communauté des bases de données aproposé un cadre formel unifiant de «semi-anneaux de provenance». L'objectif de cet articleest de certifier a posteriori la correction d’une provenance. Pour ce faire, nous proposonsune formalisation en Coq fondée sur le modèle de semi-anneaux de provenance pour desanalyses de données exprimées en algèbre relationnelle. Nous introduisons ici notammentune 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éesavec des garanties fortes de provenance