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

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

**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.

**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 Thery