A Coq formalization of data provenance - Laboratoire Méthodes Formelles Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

A Coq formalization of data provenance

Résumé

In multiple domains, large amounts of data are daily generated and combined to be analyzed. The interpretation of these analyses requires to track back the provenance of combined data with respect to initial, raw data. The correctness of the provenance is crucial in many critical domains, such as medicine to prescribe treatments. In this article, we propose the first provenance-aware extended relational algebra formalized in a proof assistant (Coq), for a non trivial subset of database queries: queries containing aggregates, null values, and correlated sub-queries. The formalization is validated by an adequacy proof with respect to standard evaluation of queries. This development is a first step towards a posteriori certification of provenance for data manipulation, with strong guaranties.
Fichier principal
Vignette du fichier
cpp21.pdf (587.44 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03380459 , version 1 (15-10-2021)

Identifiants

Citer

Véronique Benzaken, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, Rébecca Zucchini. A Coq formalization of data provenance. Certified Programs and Proofs, ACM, Jan 2021, Virtual Event, Denmark. ⟨10.1145/3437992.3439920⟩. ⟨hal-03380459⟩
91 Consultations
87 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More