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
`A Modular Formalisation of Finite Group Theory' Research Report 6156.
Laurent Théry and Guillaume Hanrot
`Primality Proving with Elliptic Curve' Research Report 6155.
`Proving the group law for elliptic curves formally' Technical Report 330.
Laurence Rideau and Laurent Théry,
`Formalising Sylow's theorems in Coq', Technical Report 327 .
` Simplifying Polynomial Expressions in a Proof Assistant', Research Report 5614 .
Proof certificates for geometry.
Fourier A reflected version of Fourier-Motzkin elimination for Coq.
Sudoku Solver: A certified solver for the Sudoku.
CoqRubik: A certified solver for the Mini Rubik.
CoqSos A port of John Harrison's Sum of Square tactic for Coq.
CoqPrime: certifying prime numbers
Propositional logic: an applet to build formulae, an applet to build natural deduction proofs.
Cyp, a proof tool to colour proofs
Aïoli, a toolkit for interactive symbolic applications.
Figue, an incremental two-dimensional layout engine.
Gbcoq, a certified implementation of Buchberger's algorithm.
CtCaml, a programming environment for CamlLight.
Chol, a proof environment for Hol
A Formal Proof that 2-Sat can be solved in linear time
A Formal Proof of Kosaraju algorithm
Hexadecimal digits of Π in Coq using the Plouffe formula
A Formal Proof in Coq of the Robbins problem.
A Formal Proof of Feit-Thompson theorem (completed on September 20, 2012).
Formalising Geometric Algebra.
A workshop on numbers and proofs in June 2006 in Paris.
A formalization in the Coq theorem prover of a Sudoku solver: paper, Coq files.
Some tactics to reason about inequalities in Coq.
A bibliography on formalised mathematics.
Some formalisations in the Coq prover.
A course on formal methods (in italian)
A course on Java and Esterel (in italian)
“ The aim of science is not to open the door to infinite wisdom, but to set a limit to infinite error. ”Bertolt Brecht