Real theorem provers deserve real user-interfaces. - Laurent Théry; Yves Bertot; Gilles Kahn (SDE, 1992)

Reasoning About the Reals: The Marriage of HOL and Maple. - John Harrison 001; Laurent Théry (LPAR, 1993)

Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. - John Harrison 001; Laurent Théry (HUG, 1993)

A Proof Development System for HOL. - Laurent Théry (HUG, 1993)

Proof by Pointing. - Yves Bertot; Gilles Kahn; Laurent Théry (TACS, 1994)

Extracting Text from Proofs. - Yann Coscoy; Gilles Kahn; Laurent Théry (TLCA, 1995)

Interactive Theorem Proving with Temporal Logic. - Amy P. Felty; Laurent Théry (J. Symb. Comput., 1997)

A Certified Version of Buchberger's Algorithm. - Laurent Théry (CADE, 1998)

A Skeptic's Approach to Combining HOL and Maple. - John Harrison 001; Laurent Théry (J. Autom. Reason., 1998)

A Generic Approach to Building User Interfaces for Theorem Provers. - Yves Bertot; Laurent Théry (J. Symb. Comput., 1998)

Formalizing Stålmarck's Algorithm in Coq. - Pierre Letouzey; Laurent Théry (TPHOLs, 2000)

A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. - Marc Daumas; Laurence Rideau; Laurent Théry (TPHOLs, 2001)

Computer validated proofs of a toolset for adaptable arithmetic - Sylvie Boldo; Marc Daumas; Claire Moreau-Finot; Laurent Théry (CoRR, 2001)

A Machine-Checked Implementation of Buchberger's Algorithm. - Laurent Théry (J. Autom. Reason., 2001)

Proving Pearl: Knuth's Algorithm for Prime Numbers. - Laurent Théry (TPHOLs, 2003)

Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs. - Laurent Théry (UITP@TPHOLs, 2003)

Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. - Yves Bertot; Laurent Théry (VSTTE, 2005)

A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. - Benjamin Grégoire; Laurent Théry (IJCAR, 2006)

A Computational Approach to Pocklington Certificates in Type Theory. - Benjamin Grégoire; Laurent Théry; Benjamin Werner (FLOPS, 2006)

Coq. - Laurent Théry; Pierre Letouzey; Georges Gonthier (The Seventeen Provers of the World, 2006)

Formalising Sylow's theorems in Coq - Laurent Théry (CoRR, 2006)

A Modular Formalisation of Finite Group Theory. - Georges Gonthier; Assia Mahboubi; Laurence Rideau; Enrico Tassi; Laurent Théry (TPHOLs, 2007)

Primality Proving with Elliptic Curves. - Laurent Théry; Guillaume Hanrot (TPHOLs, 2007)

Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. - Benjamin Grégoire; Loïc Pottier; Laurent Théry (Automated Deduction in Geometry, 2008)

Proof Pearl: Revisiting the Mini-rubik in Coq. - Laurent Théry (TPHOLs, 2008)

A distributed editing environment for XML documents - Claude Pasquier; Laurent Théry (CoRR, 2009)

A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. - Laurent Fuchs; Laurent Théry (Automated Deduction in Geometry, 2010)

Extending Coq with Imperative Features and Its Application to SAT Verification. - Michaël Armand; Benjamin Grégoire; Arnaud Spiwack; Laurent Théry (ITP, 2010)

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. - Michaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Théry; Benjamin Werner (CPP, 2011)

A Flexible Proof Format for SMT: a Proposal. - Frédéric Besson; Pascal Fontaine; Laurent Théry (PxTP, 2011)

Rigorous Polynomial Approximation Using Taylor Models in Coq. - Nicolas Brisebarre; Mioara Joldes; Érik Martin-Dorel; Micaela Mayero; Jean-Michel Muller; Ioana Pasca; Laurence Rideau; Laurent Théry (NASA Formal Methods, 2012)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

Certified, Efficient and Sharp Univariate Taylor Models in COQ. - Érik Martin-Dorel; Laurence Rideau; Laurent Théry; Micaela Mayero; Ioana Pasca (SYNASC, 2013)

Formally Verified Certificate Checkers for Hardest-to-Round Computation. - Érik Martin-Dorel; Guillaume Hanrot; Micaela Mayero; Laurent Théry (J. Autom. Reason., 2015)

Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science. - Laurent Théry; Freek Wiedijk (Math. Comput. Sci., 2015)

Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers. - Arthur Blot; Jean-Michel Muller; Laurent Théry (NSV@CAV, 2017)

Distant decimals of $π$. - Yves Bertot; Laurence Rideau; Laurent Théry (CoRR, 2017)

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. - Ran Chen; Cyril Cohen; Jean-Jacques Lévy; Stephan Merz; Laurent Théry (CoRR, 2018)

Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. - Yves Bertot; Laurence Rideau; Laurent Théry (J. Autom. Reason., 2018)

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. - Ran Chen; Cyril Cohen; Jean-Jacques Lévy; Stephan Merz; Laurent Théry (ITP, 2019)

Quantitative Continuity and Computable Analysis in Coq. - Florian Steinberg 001; Laurent Théry; Holger Thies (ITP, 2019)

Proof Pearl : Playing with the Tower of Hanoi Formally. - Laurent Théry (ITP, 2021)

Computable analysis and notions of continuity in Coq. - Florian Steinberg 001; Laurent Théry; Holger Thies (Log. Methods Comput. Sci., 2021)

A Formalisation of Algorithms for Sorting Network. - Laurent Théry (CoRR, 2022)

Primality Tests and Prime Certificate. - Laurent Théry; Sophia Antipolis (CoRR, 2022)

A Formalisation of a Fast Fourier Transform. - Laurent Théry (CoRR, 2022)