Extending Coq with Imperative Features and its Application to SAT Verification

Abstract. Coq has within its logic a programming language that can be used effectively to replace many deduction steps into a single compu-tation, this is the so-called reflection. In this paper, we present a major improvement of the evaluation mechanism that preserves its correctness and makes it possible to deal with cpu-intensive tasks such as proof checking of SAT traces.