The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Laurent Théry: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

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]


Search in 0.129secs, Finished in 0.129secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002