Extending Coq with Imperative Features and Its Application to SAT Verification
M Armand, B Grégoire, A Spiwack, L Théry - International Conference on …, 2010 - Springer
M Armand, B Grégoire, A Spiwack, L Théry
International Conference on Interactive Theorem Proving, 2010•SpringerCoq 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.
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.
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.
Springer
