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
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Cauderlier, Raphaël; Dubois, Catherine: Focalize and dedukti to the rescue for proof interoperability (2017)
- Cauderlier, Raphaël; Dubois, Catherine: ML pattern-matching, recursion, and rewriting: from focalize to dedukti (2016)
- Dubois, Catherine; Pessaux, François: Termination proofs for recursive functions in FoCaLiZe (2016)
- Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)