Coq Optimisé par son LAngage – Coqola

Les assistants de preuve sont des logiciels de recherche de pointe, qui permettent à leur utilisateur de décrire une preuve
mathématique dans un langage proche d'un langage de programmation, et vérifient que la preuve est correcte. Ils effectuent des
calculs coûteux en temps et mémoire.
Nous proposons de travailler sur l'assistant de preuve Coq, développé dans le langage de programmation OCaml. Nous voulons
améliorer conjointement Coq et OCaml en étudiant l'implémentation de Coq pour comprendre quelles nouvelles fonctionnalités pourraient être ajoutées à OCaml pour améliorer Coq et tous les autres logiciels de ce domaine. (Détails: améliorer l'optimiseur
flambda2, étendre le runtime system avec un tas isolé, immutable et hashconsé, concevoir un langage d'entrée non-typé pour le
compilateur OCaml pour l'extraction de Coq...)
Notre consortium réunit des experts académiques et industriels, à la fois de l'implémentation de Coq et de l'implémentation de OCaml
pour les faire travailler ensemble sur ce projet.
Ces outils sont de plus en plus utilisés en Cybersécurité (vérification des Critères Communs en Coq pour l'ANSSI) et en Sûreté de
Fonctionnement pour la vérification de programmes, l'absence de bugs et de vulnérabilités.