Laurent Théry

Publication Activity (10 Years)

Years Active: 1992-2022
Publications (10 Years): 12

Top Topics

Top Venues

J. Autom. Reason.

Math. Comput. Sci.

Publications

Laurent Théry
A Formalisation of a Fast Fourier Transform. CoRR (2022)
Laurent Théry
A Formalisation of Algorithms for Sorting Network. CoRR (2022)
Laurent Théry, Sophia Antipolis
Primality Tests and Prime Certificate. CoRR (2022)
Laurent Théry
Proof Pearl : Playing with the Tower of Hanoi Formally. ITP (2021)
Florian Steinberg, Laurent Théry, Holger Thies
Computable analysis and notions of continuity in Coq. Log. Methods Comput. Sci. 17 (2) (2021)
Florian Steinberg, Laurent Théry, Holger Thies
Quantitative Continuity and Computable Analysis in Coq. ITP (2019)
Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. ITP (2019)
Florian Steinberg, Laurent Théry, Holger Thies
Quantitative continuity and computable analysis in Coq. CoRR (2019)
Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. CoRR (2018)
Yves Bertot, Laurence Rideau, Laurent Théry
Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation. J. Autom. Reason. 61 (1-4) (2018)
Arthur Blot, Jean-Michel Muller, Laurent Théry
Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers. NSV@CAV (2017)
Yves Bertot, Laurence Rideau, Laurent Théry
Distant decimals of $π$. CoRR (2017)
Laurent Théry, Freek Wiedijk
Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science. Math. Comput. Sci. 9 (1) (2015)
Érik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry
Formally Verified Certificate Checkers for Hardest-to-Round Computation. J. Autom. Reason. 54 (1) (2015)
Érik Martin-Dorel, Laurence Rideau, Laurent Théry, Micaela Mayero, Ioana Pasca
Certified, Efficient and Sharp Univariate Taylor Models in COQ. SYNASC (2013)
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
A Machine-Checked Proof of the Odd Order Theorem. ITP (2013)
Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry
Rigorous Polynomial Approximation Using Taylor Models in Coq. NASA Formal Methods (2012)
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CPP (2011)
Frédéric Besson, Pascal Fontaine, Laurent Théry
A Flexible Proof Format for SMT: a Proposal. PxTP (2011)
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry
Extending Coq with Imperative Features and Its Application to SAT Verification. ITP (2010)
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)
Claude Pasquier, Laurent Théry
A distributed editing environment for XML documents CoRR (2009)
Benjamin Grégoire, Loïc Pottier, Laurent Théry
Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. Automated Deduction in Geometry (2008)
Laurent Théry
Proof Pearl: Revisiting the Mini-rubik in Coq. TPHOLs (2008)
Laurent Théry, Guillaume Hanrot
Primality Proving with Elliptic Curves. TPHOLs (2007)
Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
A Modular Formalisation of Finite Group Theory. TPHOLs (2007)
Benjamin Grégoire, Laurent Théry
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. IJCAR (2006)
Benjamin Grégoire, Laurent Théry, Benjamin Werner
A Computational Approach to Pocklington Certificates in Type Theory. FLOPS (2006)
Laurent Théry
Formalising Sylow's theorems in Coq CoRR (2006)
Yves Bertot, Laurent Théry
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. VSTTE (2005)
Laurent Théry
Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs. Electron. Notes Theor. Comput. Sci. 103 (2004)
Laurent Théry
Proving Pearl: Knuth's Algorithm for Prime Numbers. TPHOLs (2003)
Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Théry
Computer validated proofs of a toolset for adaptable arithmetic CoRR (2001)
Marc Daumas, Laurence Rideau, Laurent Théry
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. TPHOLs (2001)
Laurent Théry
A Machine-Checked Implementation of Buchberger's Algorithm. J. Autom. Reason. 26 (2) (2001)
Pierre Letouzey, Laurent Théry
Formalizing Stålmarck's Algorithm in Coq. TPHOLs (2000)
Yves Bertot, Laurent Théry
A Generic Approach to Building User Interfaces for Theorem Provers. J. Symb. Comput. 25 (2) (1998)
John Harrison, Laurent Théry
A Skeptic's Approach to Combining HOL and Maple. J. Autom. Reason. 21 (3) (1998)
Laurent Théry
A Certified Version of Buchberger's Algorithm. CADE (1998)
Amy P. Felty, Laurent Théry
Interactive Theorem Proving with Temporal Logic. J. Symb. Comput. 23 (4) (1997)
Yann Coscoy, Gilles Kahn, Laurent Théry
Extracting Text from Proofs. TLCA (1995)
Yves Bertot, Gilles Kahn, Laurent Théry
Proof by Pointing. TACS (1994)
Laurent Théry
A Proof Development System for HOL. HUG (1993)
John Harrison, Laurent Théry
Reasoning About the Reals: The Marriage of HOL and Maple. LPAR (1993)
John Harrison, Laurent Théry
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. HUG (1993)
Laurent Théry, Yves Bertot, Gilles Kahn
Real theorem provers deserve real user-interfaces. SDE (1992)