The SCEAS System
| |||||||

## 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.014secs, Finished in 0.015secs | |||||||

| |||||||

| |||||||

System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002 for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002 |