Laurent Théry


  • Organisation: INRIA
  • Research Unit: Sophia Antipolis
  • Project: MARELLE
  • Address: 2004, route des Lucioles - B.P. 93 06902 Sophia Antipolis Cedex France
  • Phone: +33 4 92 38 76 87
  • Fax: +33 4 92 38 50 29
  • E-mail:
  • PGP
  • Ftp Area
  • Emily, Jeremy

    Some Publications

    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.

    More publications


    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 group law for elliptic curves (Edwards curve). It follows the following paper by Tom Hales.

    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