Front Page

Le projet COQUILLE est terminé. Il a donné naissance à deux projets annexes : COQTAIL et COQUILLE / IDE.

Ceci est le wiki du projet COQUILLE, développé par l'équipe M1 IF de l'ENS Lyon et a pour vocation dans un premier temps de préciser les lignes directrices du projet, puis dans un second temps de faciliter le développement logiciel et la communication. Enfin, dans un futur proche, faciliter l'utilisation de la production logicielle de COQUILLE.

COQUILLE est l'acronyme de « Coq User-Interactive Library Learning Expert ». Pourquoi ?

Le forum du développement du projet est disponible sur cette page. Le site officiel du projet est plus adapté à une vue d'ensemble extérieure.

1. Faciliter l'utilisation de Coq pour la démonstration de propriétés mathématiques.
   

2. Faciliter l'utilisation de Coq par les mathématiciens non experts en calcul des constructions et en théorie des types.
   

3. Encourager l'utilisation d'assistants de preuves dans les entreprises.
   

4. Faire du coq
   

5. Augmenter la liste des propriétés démontrées en coq

Il s'agira d'augmenter la liste des théorèmes qui existent dans stdlib (ou c-corn) n'hésitez pas à approfondir ou à élaguer la liste obsolète ci-dessous.

1. État de l'art : beaucoup, beaucoup de choses existent.
   

2. Fera-t-on du constructif ? Pour l'analyse, C-CoRN ?
   

3. DOWN : Supposer des lemmes plus généraux pour paralléliser
   

4. UP : Trouver des axiomes à éliminer (Gallais ?)

1. À partir d'exemples, génération d'un arbre de décision
   

2. À partir de cet arbre, création d'une tactique

Interface en Qt, avec quelques fonctionnalités supplémentaires.

C'est l'idée originale, qui est l'aide aux prouveurs. Comme Ltac est le langage de tactiques de coq, cette partie sera probablement codée en ltac. À approfondir, mais ce WP semble mieux défini à présent.

Diffuser les résultats, c'est très important. (On le verra bien, rien que dans l'état de l'art). Liste à compléter :

1. Site web : [graal.ens-lyon.fr/coquille graal.ens-lyon.fr/coquille]
   

2. Communication interne
   

3. Rapports