Coqtail
COQ Theorems, Abstractions and Implementations (Bachelor-Level)
News
[2012-03-12] Preuve du théorème des quatres carrés de Lagrange
[26 août 2011] Talks @ Coq workshop sur une axiomatique constructive pour ℝ et la résolution d'équations différentielles par reflection
[31 juillet 2011] Talk @ THedu sur les séries entières en Coq.
[2010-2011] COQTAIL est maintenant un laboratoire junior de l'ENS Lyon.
[07 avril 2010] La première révision est maintenant disponible ! Vous pouvez la télécharger ici.
Origine & Objectifs
Le projet COQTAIL est le fils biologique du groupe de travail « Preuves » du projet COQUILLE. Il se fonde donc sur l'intégralité des résultats obtenus lors du semestre de développement de COQUILLE.
En plus d'implémenter des outils permettant une formalisation aisée des mathématiques abordées en classes préparatoires, ce projet tâchera également de démontrer des résultats de niveau licence.
Axes de développements
- Analyse (réelle et complexe)
- Arithmétique
- Calculabilité
- Implémentation de ℂ
- Logique, expressivité de l'axiomatique de ℝ
- Topologie
