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

Laurent Fuchs, Laurent 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 *.

Laurent Théry,

`Formalising Huffman's algorithm',
*Research Report*.

my android application TicTacToe TuTor that plays perfectly.

my android application Peanoware that lets you build natural deduction trees.

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 formalisation of the Generalised Towers of Hanoi

A new version of Buchberger's algorithm for Gröbner basis in Coq with Ssreflect .

A little animation Hopscotch in Scratch of the name of my research team (Marelle).

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

Floating Point Numbers and Formal Proof : 4 lectures in Coq.

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