Proving and Computing: a Certified Version of the Buchberger's Algorithm
Laurent Théry · OpenGrey (Institut de l'Information Scientifique et Technique) · 1997
This paper shows on a non-trivial example that it is possible to mix proving and computing using current technologies. We present a proof of the Buchberger's algorithm that has been developed in the Coq proof assistant. The formulation of the algorithm in Coq can then be efficiently compiled and used to do computation.