Publications before 2006

Journals:

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.

Conferences

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.

Reports:

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.

Misc.:

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.