Preuves en Coq pour la récriture de requêtes

Dans ce POM, on s’intéresse à la récriture de requêtes qui consiste à reformuler une requête en utilisant d’autre relations. Ces techniques de récriture trouvent des applications en intégration de données et en sécurité.

Concrètement, on souhaite porter une bibliothèque de récriture écrite en OCaml vers Coq, puis de prouver quelques propriétés sur le code obtenu. L’objectif étant ambitieux, on se concentrera sur certaines briques de bases: représentation des requêtes, pattern-matching et unification sur des morceaux requête.