Managing certifications in FoCaL
Renaud Rioboo (Universtité Pierre et Marie Curie)
(Joint work with Ivan Noyer)
The talk will present the FoCaL toolkit which consists of
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.
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.
back to EIDMA Seminar Combinatorial Theory announcements