Laurent Théry

[Français]

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

    Publications

    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.

    Laurent Théry,
    `` A certified version of Buchberger's algorithm'', Cade-15, LNAI 1412, Lindau 1998

    Others

    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

    Laurent Thery