A. J. Références, . Vatton-i, A. A. Arbor, and . Corporation-i, Contextual typesetting of mathematical symbols taking care of optical scaling RR-1972 Word User's Guide, ARS 97] ARSAC O., Interfaces homme machine pour le calcul formel, 1993.

A. O. and D. S. Gaëtano-m, The Design of a Customizable Component to Display and Edit Formulas, Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation (ISSAC-99), pp.283-290, 1999.

. Y. Bertot, T. L. Kahn-g, and . Y. Bertot, Proof by pointing, Direct manipulation of Algebraic Formulae in Interactive Proof Systems , Workshop on User-Interfaces for Theorem Provers Formal aspects of Computing, pp.141-97, 1994.
DOI : 10.1007/3-540-57887-0_94
URL : https://hal.archives-ouvertes.fr/inria-00073402

C. P. Borras, I. J. Despeyroux-t, L. B. Kahn-g, P. V. Bornat, and . Sufrin-b, CENTAUR: The system Animating Formal Proof at the Surface: The Jape Proof Calculator, The Computer Journal, vol.42, issue.3, pp.177-192, 1987.

. B. Buchberger, Mathematica: A system for doing mathematics by computer?, 1993.
DOI : 10.1007/BFb0013163

. J. Chlebíková, The Euromath System -The Structured Editor for Mathematicians, Proceedings of the Tenth European TeX Conference, pp.82-93, 1998.

I. L. Constable-r, A. S. , H. Bromely, C. W. Cooke-j, . T. Sobel-e et al., Implementing Mathematics with the Nuprl Development System MathWriter: mathematical typesetting with the Macintosh, FrameMaker Reference ManualCOS 96] COSCOY Y., A Natural Language Explanation for Formal Proofs Proceedings of Int. Conf. on Logical Aspects of Computational Liguistics (LACL), 1986.

D. S. Gaëtano-m and S. W. Watt-kü-chlin-w, An OpenMath 1.0 implementation, Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, pp.241-248, 1997.

D. A. , R. L. Van-egmond-s, . Heeman-f, and . J. Van-vliet, Distributed programming environments: an example of a message protocol INFORM: an interactive syntaxdirected formulae editor, Inria. [EGM The Journal of Systems and Software, vol.89, issue.9 3, pp.169-182, 1989.

G. M. Melham-t, . R. Hersch, . G. Huet, . Kahn-g, and . C. Paulin-mohring, Introduction to HOL: A theorem proving environment for higher order logic Visual and Technical Aspects of Type The Coq Proof Assistant : A Tutorial : Version 6, 1993.

. N. Kajler and W. P. Cas-/, CAS/PI, Papers from the international symposium on Symbolic and algebraic computation , ISSAC '92, pp.376-386, 1992.
DOI : 10.1145/143242.143359

. N. Kajler, User interfaces for symbolic computation, Proceedings of the 6th annual ACM symposium on User interface software and technology , UIST '93, pp.1-10, 1993.
DOI : 10.1145/168642.168643

. N. Kajler and . Soiffer-n, A Survey of User Interfaces for Computer Algebra Systems, Journal of Symbolic Computation, vol.25, issue.2, pp.127-160, 1998.
DOI : 10.1006/jsco.1997.0170

. E. Kaltofen, . Watt-s, . Computers, . Mathematics, and . Springerverlag, Computers and Typesetting, KNU 89] KNUTH D., Typesetting Concrete Mathematics , TUGboat, pp.31-36, 1986.

K. D. Kosmala, L. S. Pottier-l, and R. G. , The TeX-Book (revised) On-Line Handwritten Formula Recognition using Hidden Markov Models and Context Dependent Graph Grammars, 5th International Conference on Document Analysis and Recognition, 1990.

L. J. Lett-g, . Mccarthy-e, L. J. Holland-c, . F. Of, . Software-s et al., Using MathML to Describe Numerical Computations, MathML International Conference extended abstract. [MAT] MathML, 1985.

. N. Ohtake, . Fukuda-r, and . Suzuki-m, Optical Recognition and Braille Transcription of Mathematical Documents, 7th International Conference on Computers Helping People with Special Needs ICCHP, 2000.

. H. Oka-99-]-okamura, C. W. Kanahori-t, . Fukuda-r, . Tamari-f, and . Suzuki-m, Handwriting Interface for Computer Algebra Systems, Fourth Asian Technology Conference in Mathematics, pp.291-300, 1999.

. Pau and . C. Paulson-l, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, p.321, 1994.

Q. V. Vatton-i, . Bedor-h, D. J. Grif:-an-interactive-environment-for-t-e-x, S. For, and . Documentation, Second European Confe- INRIA rence, Lecture Notes in Computer Science, pp.145-158, 1986.

. P. Rosier, Développement d'un environnement de programmation Centaur pour Maple, 1995.

S. D. Mathtype-user-manual and S. C. Soiffer-n, [SMA] SmarTools , http://www-sop.inria.fr/oasis MathScribe: A User INterface for Computer Algebra Systems, Proceedings of the 1986 Symposium on Symbolic and Algebriaic Computation, pp.7-13, 1986.

T. T. Equationbuilder-user-manual, T. T. , and R. T. , The Cornell Program Synthesizer: a sunyntax-directed Programming Environment, Communications of the ACM, vol.24, issue.9, pp.152-168, 1981.

T. L. And-bertot-l, . And, and . Kahn-g, Real Theorem Provers Deserve Real User-Interfaces, Proceedings of the Fifth ACM Symposium on Software Development Environments (SDE5), pp.283-290, 1992.

. Unité-de-recherche-inria-sophia and . Antipolis, 93 -06902 Sophia Antipolis Cedex (France) Unité de recherche INRIA Lorraine : Technopôle de Nancy-Brabois -Campus scientifique 615, rue du Jardin Botanique -B.P. 101 -54602 Villers lès Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38330, France) Unité de recherche INRIA Rocquencourt : Domaine de Voluceau -Rocquencourt -B.P. 105 -78153 Le Chesnay Cedex, 2004.

I. De-voluceau-rocquencourt and B. P. , 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399