The talk will present the FoCaL toolkit which consists of
-
a language (FoCaL) enabling to specify function, states there properties but also to implement these functions and prove their properties.
-
A compiler producing ocaml and Coq sources.
-
An automatic prover (Zenon) which eases the process of certifying function properties.
We will emphasize on tools which enable to provide online mathematical documentation for FoCaL sources viewable using a simple Web browser which uses the MathML standard. These tools also enable to explore parts of the library and to share values with other softwares using the OpenMath standard.
|