The prototype is accessible via a Web interface.
Mowgli's prototype was tested on the Java Card formal model, which contains more than 3750 formal definitions and 2000 theorems along 4MB of Coq source code. The intended purpose was to test Mowgli as a support for explaining those models to the evaluator.
Trusted Logic developed a tool for retrieving source information as meta-data. This includes several kinds of information that present in the sources but that is not part of logical terms, like comments on the formal definitions included in the source files, coercions, implicit arguments, derived constants, etc.
Download the meta-data extractor for CIC terms.
The second contribution that Trusted Logic developed is an SPM document of GlobalPlatform, a widely used card manager standard for smart cards.
Download the XML files containing the SPM document.
The third contribution that Trusted Logic developed is related to the use of Mowgli's XML output as an exchange format for formal models.
Download the sources of the translator from Coq to UML or look at some screen-shots of its output in Rational Rose [gp-comm.png, gp-install.png, tables-relations.png, tables.png].
GtkMathView is a GTK+ component for rendering MathML documents. The
component can be customized as to react to user events such as clicking
The home page of the component, along with online documentation, dependencies, instructions for compilation, can be found here.
Hermes is a content oriented LaTeX authoring tool for scientific articles;
it converts the LaTeX source into XML with Content-MathML islands.
The home page of the converter, along with documentation and samples, can be found here.