Laboratoire de langages et outils de programmation

Cypher’s Mechanization

Formalisation de Cypher, un langage de requête graphique, dans Coq.

Ce projet vise à formaliser Cypher, un langage de requête graphique, dans l'assistant de preuve Coq. L'objectif de la formalisation est de poser des bases solides pour l'évolution du langage, ansi que de créer un créer un cadre de vérification des optimisations de requêtes.

Participants

Anton Podkopaev