B. R. Sufrin-b, Animating Formal Proof at the Surface : The Jape Proof Calculator, The Computer Journal, vol.42, issue.3, pp.177-192, 1999.

B. B. Mathematica, A System for Doing Mathematics by Computer ?, 1993.

C. J. Sobel-e, MathWriter : mathematical typesetting with the Macintosh, 1986.

V. S. Egmond, . Heeman-f, and . J. Van-vliet, INFORM: An interactive syntax-directed formulae editor, Journal of Systems and Software, vol.9, issue.3, pp.169-182, 1989.
DOI : 10.1016/0164-1212(89)90037-X

G. M. Melham-t, Introduction to HOL : A theorem proving environment for higher order logic, 1993.

H. G. Kahn-g and . C. Paulin-mohring, « The Coq Proof Assistant : A Tutorial : Version 6, 1997.

K. N. and «. Cas, PI : a portable and extensible interface for computer algebra systems, Proceedings of ISSAC '92. International Symposium on Symbolic and Algebraic Computation, pp.376-386, 1992.

K. N. Soiffer-n, Survey of User Interfaces for Computer Algebra Systems, Journal of Symbolic Computation, vol.25, issue.2, pp.127-160, 1998.

K. A. , L. S. Pottier-l, and R. G. , « On-Line Handwritten Formula Recognition using Hidden Markov Models and Context Dependent Graph Grammars, 5th International Conference on Document Analysis and Recognition, 1999.

O. N. 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.

S. C. Soiffer-n, A User INterface for Computer Algebra Systems, Proceedings of the 1986 Symposium on Symbolic and Algebriaic Computation, pp.7-13, 1986.