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