Laurent Théry

[Français]

  • Organisation: INRIA
  • Research Unit: Sophia Antipolis
  • Project: CROAP
  • Phone: +33 4 92 38 78 16
  • Fax: +33 4 92 38 76 33
  • E-mail: Laurent.Thery@inria.fr

    Cv,Publications, Software,

    Publications

    Journals:

    John Harrison and Laurent Théry,
    ``A Skeptic's Approach to Combining Hol and Maple'', Journal of Automated Reasoning (1998) 21 pp 279-294.

    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,
    ``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:

    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.

    Software

    Aïoli, a toolkit for interactive symbolic applications.

    Figue, an incremental two-dimensional layout engine.

    Gbcoq, a certified implementation of Buchberger's algorithm.

    CtCaml, a programming environment for CamlLight.

    Chol, a proof environment for Hol