Extending Coq with Imperative Features and its Application to SAT Verification

Michaël Armand 1 Benjamin Grégoire 1 Arnaud Spiwack 2, 3 Laurent Théry 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Coq has within its logic a programming language that can be used to replace many deduction steps into a single computation, this is the so-called reflection. In this paper, we present two extensions of the evaluation mechanism that preserve its correctness and make it possible to deal with cpu-intensive tasks such as proof checking of SAT traces.
Type de document :
Communication dans un congrès
Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00502496
Contributeur : Arnaud Spiwack <>
Soumis le : jeudi 26 août 2010 - 11:51:20
Dernière modification le : jeudi 11 janvier 2018 - 16:38:52
Document(s) archivé(s) le : mardi 23 octobre 2012 - 15:06:27

Fichier

fastcoq.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00502496, version 2

Collections

Citation

Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry. Extending Coq with Imperative Features and its Application to SAT Verification. Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. 2010. 〈inria-00502496v2〉

Partager

Métriques

Consultations de la notice

343

Téléchargements de fichiers

173