The FOC research project is building a development environment for certified computer algebra. It offers a concrete syntax allowing to write programs, to declare properties and to prove them. The environment is organized as a hierarchy of packages, which can be extended by refinement, multiple inheritance and late binding. A formal specification of this hierarchy and of its tools has been done with the theorem prover Coq and has shown that non-controlled uses of these tools can lead to inconsistencies. The control is done by a static analysis of the FOC code, which serves also for the compilation to executable code on one side (via OCaml) and to a proof term (checked by Coq) on the other side. During the talk, I shall give an overview of FOC and I will focus on the dependecies management through the static analysis.