Search the dblp DataBase

Publications of Author

1. Benjamin Grégoire, Laurent Théry
   A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. [Citation Graph (0, 0)][DBLP]
   IJCAR, 2006, pp:423-437 [Conf]
   
2. Laurent Théry
   A Certified Version of Buchberger's Algorithm. [Citation Graph (0, 0)][DBLP]
   CADE, 1998, pp:349-364 [Conf]
   
3. Benjamin Grégoire, Laurent Théry, Benjamin Werner
   A Computational Approach to Pocklington Certificates in Type Theory. [Citation Graph (0, 0)][DBLP]
   FLOPS, 2006, pp:97-113 [Conf]
   
4. John Harrison, Laurent Théry
   Reasoning About the Reals: The Marriage of HOL and Maple. [Citation Graph (0, 0)][DBLP]
   LPAR, 1993, pp:351-353 [Conf]
   
5. Yves Bertot, Gilles Kahn, Laurent Théry
   Proof by Pointing. [Citation Graph (0, 0)][DBLP]
   TACS, 1994, pp:141-160 [Conf]
   
6. Yann Coscoy, Gilles Kahn, Laurent Théry
   Extracting Text from Proofs. [Citation Graph (0, 0)][DBLP]
   TLCA, 1995, pp:109-123 [Conf]
   
7. Marc Daumas, Laurence Rideau, Laurent Théry
   A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2001, pp:169-184 [Conf]
   
8. John Harrison, Laurent Théry
   Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. [Citation Graph (0, 0)][DBLP]
   HUG, 1993, pp:174-184 [Conf]
   
9. Pierre Letouzey, Laurent Théry
   Formalizing Stålmarck's Algorithm in Coq. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:388-405 [Conf]
   
10. Laurent Théry
    Proving Pearl: Knuth's Algorithm for Prime Numbers. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:304-318 [Conf]
    
11. Laurent Théry
    A Proof Development System for HOL. [Citation Graph (0, 0)][DBLP]
    HUG, 1993, pp:115-128 [Conf]
    
12. Laurent Théry, Pierre Letouzey, Georges Gonthier
    Coq. [Citation Graph (0, 0)][DBLP]
    The Seventeen Provers of the World, 2006, pp:28-35 [Conf]
    
13. Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Théry
    Computer validated proofs of a toolset for adaptable arithmetic [Citation Graph (0, 0)][DBLP]
    CoRR, 2001, v:0, n:, pp:- [Journal]
    
14. Laurent Théry
    Colouring Proofs: A Lightweight Approach to Adding Formal Structure to Proofs. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 2004, v:103, n:, pp:121-138 [Journal]
    
15. John Harrison, Laurent Théry
    A Skeptic's Approach to Combining HOL and Maple. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 1998, v:21, n:3, pp:279-294 [Journal]
    
16. Laurent Théry
    A Machine-Checked Implementation of Buchberger's Algorithm. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2001, v:26, n:2, pp:107-137 [Journal]
    
17. Yves Bertot, Laurent Théry
    A Generic Approach to Building User Interfaces for Theorem Provers. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 1998, v:25, n:2, pp:161-194 [Journal]
    
18. Amy P. Felty, Laurent Théry
    Interactive Theorem Proving with Temporal Logic. [Citation Graph (0, 0)][DBLP]
    J. Symb. Comput., 1997, v:23, n:4, pp:367-397 [Journal]
    
19. Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
    A Modular Formalisation of Finite Group Theory. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2007, pp:86-101 [Conf]
    
20. Laurent Théry, Guillaume Hanrot
    Primality Proving with Elliptic Curves. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2007, pp:319-333 [Conf]
    
21. Laurent Théry
    Formalising Sylow's theorems in Coq [Citation Graph (0, 0)][DBLP]
    CoRR, 2006, v:0, n:, pp:- [Journal]
    
22. 
    Proof Pearl: Revisiting the Mini-rubik in Coq. [Citation Graph (, )][DBLP]
    
    
23. 
    Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. [Citation Graph (, )][DBLP]
    
    
24. 
    Extending Coq with Imperative Features and Its Application to SAT Verification. [Citation Graph (, )][DBLP]
    
    
25. 
    A distributed editing environment for XML documents [Citation Graph (, )][DBLP]