Mathematical Knowledge Management in Foc

We present a library which enables to implement general computer algebra notions called here entities, collections and species without the help of a dedicated language. We give an operational model for these notions, which has been formalized and veri ed using the Coq proof assistant. We rely on this model to design the programming discipline of the library. This allows us to produce semantically founded programs in a general purpose language (Ocaml). Thus, a lot of programming features such as polymorphism, type inference, data structure management, garbage collection are obtained for free while keeping good eciency when running computer algebra algorithms. The discipline corresponds to a restricted use of \object oriented" together with \module" features, which is formalized in the theorem prover Coq. Following the discipline is enforced by the concrete syntax given to users