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.
Type de document :
Rapport
RR-3275, INRIA. 1997
Liste complète des métadonnées

https://hal.inria.fr/inria-00073414
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:44:40
Dernière modification le : samedi 27 janvier 2018 - 01:31:30
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:45:49

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

83

Téléchargements de fichiers

118