FoCaLiZe is an environment for specifying, programming and proving. It has been developed for more than 15 years, it supports different kinds of applications, the first testbed application being the development of formally verified computer algebra libraries. In this talk I will present the main ingredients and the architecture of FoCaLiZe, that is more precisely the features of the eponym language, the dependency calculus and the different backends—OCaml, Coq and Dedukti—allowing for code execution and verification of proofs. The tour will finished with the demonstration that FoCaLiZe can help to combine proofs coming from different theorem provers, e.g. HOL Light and Coq, thanks to its Dedukti backend and structuring features like inheritance and parametrization.

Joint work with the FoCaLiZe development team (in particular Raphaël Cauderlier, Thérèse Hardin, Renaud Rioboo, François Pessaux, Virgile Prevosto).