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

  • 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.

back to EIDMA Seminar Combinatorial Theory announcements