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.