``A Machine-Checked Implementation of Buchberger's Algorithm'',

``A Skeptic's Approach to Combining Hol and Maple'',

**Yves Bertot and Laurent Théry**,

``A Generic Approach to Building User Interfaces for Theorem Provers'',
*Journal of Symbolic Computation (1998) 25, pp 161-194*.

**Amy Felty and Laurent Théry**,

``Interactive Theorem Proving with Temporal Logic'',
* Journal of Symbolic Computation (1997) 23, pp 367-397*.

Laurent Théry,

'Formalising Huffman's algorithm',
*Technical Report 034*,

Laurent Théry,

'Colouring proofs: a lightweight approach to adding formal structure to proofs',
*ENTCS*,

Laurent Théry,

`A Table-Driven Compiler for Pretty Printing Specifications',
*Technical Report 288*.

Laurent Théry,

`Proving Pearl: Knuth's algorithm for prime numbers',
*TPHOLs 2003, LNCS 2758*,

Sylvie Boldo, Marc Daumas, Laurent Théry,

`Formal proofs and computations in finite
precision arithmetic',
*Calculemus 2003*.

Laurent Théry,

`Formal Proof Authoring: an Experiment',
*UITP 2003*.
Marc Daumas, Laurence Rideau and Laurent Théry,

`A Generic Library for Floating-Point Numbers and its
Application to Exact Computing',
*TPHOLs2001, LNCS 2152 pp 169-184*.

** Pierre Letouzey and Laurent Théry**,

``Stalmarck's algorithm in Coq',
*TPHOLs2000, LNCS 1869 pp 387-404*.

**Laurent Théry**,

``
A certified version of Buchberger's algorithm'',
*Cade-15, LNAI 1412, Lindau 1998*

**Yann Coscoy, Gilles Kahn, and Laurent Théry**,

``Extracting Text from Proof'',
* Typed Lambda-Calculi and Applications (TLCA `95) LNCS 902*,
Edinburgh, April 1995.

**Yves Bertot, Gilles Kahn, and Laurent Théry**,

``Proof by Pointing''
*Symposium on Theoretical Aspects Computer Software (STACS)*,
Sendai (Japan), LNCS 789, April 1994.

**John Harrison, Laurent Théry**,

``Reasoning about the Reals: the marriage of HOL and Maple'',

* International conference on Logical Programming and Automated Reasoning*, St Petersburg, 1993.

**John Harrison, Laurent Théry**,

``Extending the HOL theorem prover with a Computer Algebra System
to Reason about the Reals'',

* International Workshop on Higher Order Logic and its applications *,
Vancouver, 1993.

** Laurent Théry,**

``A proof development system for the HOL theorem prover'',

* International Workshop on Higher Order Logic and its applications *,
Vancouver, 1993.

**Laurent Théry, Yves Bertot, and Gilles Kahn**,

``Real Theorem Provers Deserve Real User-Interfaces''

*The Fifth ACM Symposium on Software Development Environments (SDE5)*,
Washington D. C., December 1992.

Laurent Théry,

`A Tour of Formal Verification with Coq:Knuth's Algorithm for Prime Numbers',
*INRIA Report 4600*, November 2002.

Laurent Théry,

`Stålmarck's Algorithm in Coq: A Three-Level Approach',
*INRIA Report 4353*, March 2002.

**Laurence Rideau and Laurent Théry**,

``Interactive Programming Environment for ML'',
INRIA Research Report no. 3139, March 1997.

**Amy Felty and Laurent Théry**,

``Interactive Theorem Proving with Temporal Logic'',
INRIA Research Report no. 2804, February 1996.

**Yann Coscoy, Gilles Kahn, and Laurent Théry**,

``Extracting Text from Proof'',
INRIA Research Report no. 2459,
January 95.

**Yves Bertot, Gilles Kahn, and Laurent Théry**,

``Proof by Pointing'', Cambridge University Research Report, December 1993.

**Laurent Théry, Yves Bertot, and Gilles Kahn**,

``Real Theorem Provers Deserve Real User-Interfaces'',
INRIA Research Report no. 1684, May 1992.

**Laurent Théry**, (*french*)

``Une méthode distribuée de création d'interfaces et ses applications aux démonstrateurs de théorèmes''
,

*PhD*, university Denis Diderot,
February 1994.

Laurent Théry Last modified: Fri Oct 17 12:43:34 MET DST 2003