|
Search the dblp DataBase
Laurent Théry:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
Publications of Author
- 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]
- Laurent Théry
A Certified Version of Buchberger's Algorithm. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:349-364 [Conf]
- 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]
- 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]
- Yves Bertot, Gilles Kahn, Laurent Théry
Proof by Pointing. [Citation Graph (0, 0)][DBLP] TACS, 1994, pp:141-160 [Conf]
- Yann Coscoy, Gilles Kahn, Laurent Théry
Extracting Text from Proofs. [Citation Graph (0, 0)][DBLP] TLCA, 1995, pp:109-123 [Conf]
- 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]
- 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]
- Pierre Letouzey, Laurent Théry
Formalizing Stålmarck's Algorithm in Coq. [Citation Graph (0, 0)][DBLP] TPHOLs, 2000, pp:388-405 [Conf]
- Laurent Théry
Proving Pearl: Knuth's Algorithm for Prime Numbers. [Citation Graph (0, 0)][DBLP] TPHOLs, 2003, pp:304-318 [Conf]
- Laurent Théry
A Proof Development System for HOL. [Citation Graph (0, 0)][DBLP] HUG, 1993, pp:115-128 [Conf]
- Laurent Théry, Pierre Letouzey, Georges Gonthier
Coq. [Citation Graph (0, 0)][DBLP] The Seventeen Provers of the World, 2006, pp:28-35 [Conf]
- 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]
- 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]
- 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]
- 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]
- 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]
- 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]
- 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]
- Laurent Théry, Guillaume Hanrot
Primality Proving with Elliptic Curves. [Citation Graph (0, 0)][DBLP] TPHOLs, 2007, pp:319-333 [Conf]
- Laurent Théry
Formalising Sylow's theorems in Coq [Citation Graph (0, 0)][DBLP] CoRR, 2006, v:0, n:, pp:- [Journal]
Proof Pearl: Revisiting the Mini-rubik in Coq. [Citation Graph (, )][DBLP]
Dependent Types, Theorem Proving, and Applications for a Verifying Compiler. [Citation Graph (, )][DBLP]
Extending Coq with Imperative Features and Its Application to SAT Verification. [Citation Graph (, )][DBLP]
A distributed editing environment for XML documents [Citation Graph (, )][DBLP]
Search in 0.004secs, Finished in 0.005secs
|