GALLINETTE

L'EPI Gallinette vise à développer une nouvelle génération d'assistants à la preuve, avec la conviction que les expériences pratiques doivent aller de pair avec les investigations fondamentales:
 

• L'objectif est de faire progresser les assistants à la preuve à la fois en tant que langages de programmation certifiés et systèmes logiques mécanisés. La programmation avancée et les paradigmes mathématiques doivent être intégrés, notamment types dépendants et effets. L'approche distinctive consiste à implémenter une nouvelle programmation et des paradigmes logiques au-dessus de Coq en considérant cette dernière comme un langage cible pour la compilation.

• Le but des recherches plus fondamentales est d'étendre les limites de la correspondance de Curry-Howard. Elle est considérée à la fois comme une base pour les langages de programmation et la logique, et comme un fournisseur de techniques essentielles au développement des assistants de preuve. Dans cette perspective, le développement d'assistants à la preuve est vu comme une expérience totale utilisant la correspondance dans tous les aspects: les langages de programmation, la théorie des types, la théorie de la preuve, la réécriture et l'algèbre.