The FoC language is dedicated to produce computer algebra libraries which are both certified and efficient. Starting from FoC sources, static analysis computes dependencies graphs, selects and remove implementations in order to resolve multiple inheritance and dependency checks. These checks enable to produce efficient Ocaml source code which can be executed. The compiler also produces a Coq environment where the programmer can certify his FoC programs.
In such an environment a programmer can hardly know which functions are selected, which are available and what they do. The FoCDoc documentation format has been recently produced in order to enable the programmer to have a readable "synopsis" of what a given compiler unit offers. The FoCDoc format produced by the compiler is specified in a DTD which enables translation into other formats.
We will present a joint work with Yvan Noyer (an MKM sponsored student) which performs a translation form the FoCDoc format into MathML format. The result is viewable using almost any MathML enabled browser such as recent versions of Mozilla.