Towards a certified and efficient computing of Gröbner bases

In this paper, we present an example of the implementation and verification of a functional program. We expose an experience in developing an application in the area of symbolic computation: the computing of Grobner basis of a set of multivariate polynomials. Our aim is the formal certification of several aspects of the program written in the functional language CAML. In addition, efficient computing of the algorithm is another issue to take into account.