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.
Laurent Théry,
`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 .
Laurent Théry,
` 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
Formalising Feit-Thompson theorem.
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)