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