The FoCaLiZe project aims at providing a programming environment to develop certified programs. The environment is based on a functional programming language with object-oriented features. The language allows the programmer to write formal specifications and proofs of the program in a unified and consistent setting. From a FoCaLiZe source code development, the focalizec compiler produces three source files: a source file for the Coq proof assistant to check the proofs, a source file for the OCaml compiler to build the executable program, a source file that contains the documentation extracted from the development sources. Thanks to built-in inheritance mechanisms, the language allows to refine a development from the coarse-grain specification to the fully defined executable program. The FoCaLiZe distribution includes a library of mathematical algebraic structures up to multivariate polynomial rings, a library of security policies and various examples contributed by FoCaLiZe users. The resulting libraries are noticeably efficient; for instance, the complex algorithms of the algebraic library provide runtime performances comparable to the best Computer Algebra Systems available.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element