On the way to certify Computer Algebra Systems
Sylvain Boulmé, Thérèse Hardin, D. Hirschkoff, Valérie Ménissier-Morain, Renaud Rioboo · Electronic Notes in Theoretical Computer Science · 1999
The FOC project, started at the fall 1997, is aimed to build a programming environment for the development of certified symbolic computation. The working languages are Coq and Ocaml. In this paper, we present first the motivations of the project. We then explain why and how our concern for proving properties of programs has led us to certain implementations choices in Ocaml. This way, the sources express exactly the mathematical dependencies between the different structures. This may ease the achievement of proofs.