Extending Coq with Imperative Features and its Application to SAT Verification - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

Extending Coq with Imperative Features and its Application to SAT Verification

(1) , (1) , (2, 3) , (1)
1
2
3

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.
Fichier principal
Vignette du fichier
fastcoq.pdf (188.29 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00502496 , version 1 (15-07-2010)
inria-00502496 , version 2 (26-08-2010)

Identifiers

  • HAL Id : inria-00502496 , version 2

Cite

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. ⟨inria-00502496v2⟩
424 View
470 Download

Share

Gmail Facebook Twitter LinkedIn More