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


https://hal.inria.fr/inria-00502496
Contributeur : Arnaud Spiwack <>
Soumis le : jeudi 26 août 2010 - 11:51:20
Dernière modification le : jeudi 9 février 2017 - 15:10:40
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

327

Téléchargements du document

161