Skip to Main content Skip to Navigation
Conference papers

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
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Arnaud Spiwack Connect in order to contact the contributor
Submitted on : Thursday, August 26, 2010 - 11:51:20 AM
Last modification on : Thursday, January 20, 2022 - 5:30:46 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 3:06:27 PM


Files produced by the author(s)


  • HAL Id : inria-00502496, version 2



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⟩



Les métriques sont temporairement indisponibles