Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
`A Modular Formalisation of Finite Group Theory'
Rapport de Recherche 6156.
Laurent Théry et Guillaume Hanrot
`Primality Proving with Elliptic Curves'
Rapport de Recherche 6155.
Laurent Théry,
`Proving the group law for elliptic curves formally'
Rapport Technique 330.
Laurence Rideau et Laurent Théry,
`Formalising Sylow's theorems
in Coq',
Rapport Technique 327 .
Laurent Théry,
` Simplifying Polynomial Expressions in a Proof Assistant',
Rapport de Recherche 5614.
Des certificats de preuve pour la géometrie.
Fourier une version par réflection de l'élimination de Fourier-Motzkin pour l'arithmetique linéaire en Coq.
Sudoku Solver: A programme certifié qui résoud les Sudoku.
CoqRubik: A programme certifié qui résoud le Mini Rubik.
CoqSos un traduction du programme de somme de carrés de John Harrison pour Coq.
CoqPrime: certifier des nombres premiers
Logique propositionnelle: une applet pour construire des formules, une applet pour construire des arbres de preuve en déduction naturelle.
Cyp, un outil pour colorier les preuves
Aïoli, une boîte à outils de construction d'applications interactives.
Figue, un moteur d'affichage bi-dimensionnel et incrémental..
Gbcoq, une implémentation certifiée de l'algorithme de Buchberger.
CtCaml, un environnement de programmation pour CamlLight.
Chol, un environnement de preuve pour Hol
Formalisation du théorème de Feit-Thompson.
Formalisation des algèbres géométriques. Résoudre le mini Rubik cube.
Une formalisation dans l'assistant de preuve Coq d'un programme qui resoud les Sudoku: le papier et les fichiers Coq.
Des tactiques pour manipuler des inégalités en Coq.
Une bibliographie des mathématiques formalisées sur machine.
Des formalisations en Coq produites par l'outil CoqDoc.
Un cours donné sur les méthodes formelles dans une université italienne (en italien).
Un cours donné sur Java et Esterel dans une université italienne (en italien).
Une introduction de preuve donnée à l'ISIA en Mars 2002. Transparents (Ps, Html ou PowerPoint).
Un exposé sur la mécanisation des preuves en arithmétique flottante donnée à l'école de printemps sur l'arithmétique des ordinateurs en Mars 2001. Transparents ou Note
Des transparents en anglais décrivant l'intégration de l'algorithme de Stålmarck en Coq(PowerPoint,Html).
Une formalisation de l'algorithme de Stålmarck en Coq.
La même preuve de RSA dans différents systèmes de preuve pour l'école d'été Types 99:
Grâce à H. Persson, une nouvelle implémentation certifiée de l'algorithme de Buchberger utilisant une preuve 100% constructive.
Quelques exercises en Coq.