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
Laurent Théry and Guillaume Hanrot
Laurent Théry,
Laurence Rideau and Laurent Théry,
Laurent Théry,
Laurent Théry,
:
`A Modular Formalisation of Finite Group Theory'
Research Report 6156.
`Primality Proving with Elliptic Curve'
Research Report 6155.
`Proving the group law for elliptic curves formally'
Technical Report 330.
`Formalising Sylow's theorems
in Coq',
Technical Report 327 .
` Simplifying Polynomial Expressions in a Proof Assistant',
Research Report 5614 .
`Formalising Huffman's algorithm',
Research Report.
Software
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