Coquille (Coq User-Interactive Library Learning Expert) est élaboré à partir de l’assistant de preuves Coq par des M1 d'Informatique Fondamentale de l'ÉNS Lyon. L’objectif est en somme d’élargir la portée de Coq aux mathématiques de classes préparatoires, et à des mathématiciens non forcément experts en calcul des constructions et en théorie des types.
Champs d'investigation
Faciliter l'implémentation de preuves formelles
- Formalisation de concepts de base et de lemmes les manipulant
- Méta-heuristique visant la génération de preuves automatiques
- Interface graphique agréable et ergonomique
Résoudre des problèmes de niveau prépa
- Bibliothèques de résultats non triviaux de niveau Licence
- Tactiques puissantes se fondant sur ces résultats
