Emily, Jeremy

## Publications

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*.

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 *.

More publications

## Software

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

## Misc

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

Laurent Théry