Skip to Main content Skip to Navigation
Reports

Proving and Computing: a Certified Version of the Buchberger's Algorithm

Laurent Théry 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073414
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 12:44:40 PM
Last modification on : Wednesday, January 8, 2020 - 11:04:18 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:45:49 PM

Identifiers

  • HAL Id : inria-00073414, version 1

Collections

Citation

Laurent Théry. Proving and Computing: a Certified Version of the Buchberger's Algorithm. RR-3275, INRIA. 1997. ⟨inria-00073414⟩

Share

Metrics

Record views

96

Files downloads

202