GhostRewriter

Les assistants à la preuve (ou prouveurs interactifs) sont utilisés pour résoudre des problèmes à la fois en mathématique et en informatique. La notion de calcul sur laquelle un grand nombre d'entre eux repose permet d'améliorer leur efficacité et les rend plus pratiques. Cependant, ils n'offrent pas suffisamment de contrôle de ce calcul. Le but de ce projet est de tirer profit de la notion de donnée fantôme (provenant du domaine de la vérification déductive) pour fournir davantage de contrôle sur le calcul. Ceci devrait permettre des développements de preuve plus expressifs et plus modulaires.