A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
A Machine-Checked Proof of the Odd Order Theorem
Primality Proving with Elliptic Curves
Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Théry Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle Research Report.
Yves Bertot, Laurence Rideau, Laurent Théry Distant Decimals of π: Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation Journal of Automated Reasoning, Volume 61 Issue 1-4, June 2018
Laurent Fuchs, Laurent Théry,
Implementing Geometric Algebra Products with Binary Trees,
Advances in Applied Clifford Algebras, 2014, Volume 24, Number 2, Page 589
L. Fuchs, L. Théry: A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. Automated Deduction in Geometry 2010.
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
Laurent Théry et Guillaume Hanrot
Laurent Théry,
Laurence Rideau et Laurent Théry,
Laurent Théry,
Laurent Théry,
Mon application android Morpion Mentor qui joue parfaitement au morpion.
Mon application android Peanoware qui permet de construire des arbres de déduction naturelle.
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
Un atelier sur le Rubik Cube à la fête de la science 2017.
Une formalisation de la loi de groupe pour les courbes elliptiques (les courbes d'Edwards). C'est une formalisation
directe d'un papier de Tom Hales.
Une formalisation d'une généralisation des tours d'Hanoi.
Mon exposé Devenez un champion de Moripon Fête de la Science 2016.
Une nouvelle version de l'algorithme de Buchberger pour les bases de Gröbner
dans Coq avec Ssreflect .
Une petite animation Hopscotch in Scratch
du nom de mon équipe de recherche: Marelle.
2-Sat peut être résolu en temps linéaire
Une preuve formelle de l'algorithme de Kosaraju
Les décimales de Π en Coq en utilisant la formule de Plouffe
Une preuve formelle en Coq du problème de Robbins.
un mini-cours virgule flottante et preuve.
Une Preuve Formelle du théorème de Feit-Thompson (terminé le 20 Septembre 2012).
Formalisation des algèbres géométriques.
Une formalisation dans l'assistant de preuve Coq d'un programme
qui résoud 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 exercices en Coq.
`A Modular Formalisation of Finite Group Theory'
Rapport de Recherche 6156.
`Primality Proving with Elliptic Curves'
Rapport de Recherche 6155.
`Proving the group law for elliptic curves formally'
Rapport Technique 330.
`Formalising Sylow's theorems
in Coq',
Rapport Technique 327 .
` Simplifying Polynomial Expressions in a Proof Assistant',
Rapport de Recherche 5614.
`Formalising Huffman's algorithm',
Research Report.
Laurent Théry