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 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)
- Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
- Müller, Dennis; Rabe, Florian; Kohlhase, Michael: Theories as types (2018)
- 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)
- Dowek, Gilles: Deduction modulo theory (2015)
- Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
- Ronan Saillard: Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice (2015) not zbMATH
- Ayrault, Philippe; Hardin, Thérèse; Pessaux, François: Development of a generic voter under FoCal (2009) ioport