Details:

Title	Proving and computing: a certified version of the Buchberger 's algorithm
Author(s)	Laurent Thery
Type	Technical Report, Misc
Abstract	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.
File
Language	English
Number	3275
Year	1997
Month	October
Edition	0
Translation	No
Refereed	No
Institution	INRIA