| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Extending Coq with Imperative Features and its Application to SAT Verification
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.
Cited literature [18 references]
https://hal.inria.fr/inria-00502496
Contributor : Arnaud Spiwack <>
Submitted on : Thursday, August 26, 2010 - 11:51:20 AM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 3:06:27 PM
Contributor : Arnaud Spiwack <>
Submitted on : Thursday, August 26, 2010 - 11:51:20 AM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Tuesday, October 23, 2012 - 3:06:27 PM
File
fastcoq.pdf
Files produced by the author(s)