Extending Coq with Imperative Features and Its Application to SAT Verification
Extending Coq with Imperative Features and Its Application to SAT Verification
复制标题
DOI：
10.1007/978-3-642-14052-5_8
复制
发表时间：
2010-07
期刊：
影响因子：
--
通讯作者：
Michaël Armand;B. Grégoire;A. Spiwack;L. Théry
中科院分区：
文献类型：
--
作者：
Michaël Armand;B. Grégoire;A. Spiwack;L. Théry
Coq在其逻辑中有一种编程语言，可以用来将许多演绎步骤替换为一次计算，这就是所谓的反射。在本文中，我们提出了两个评估机制的扩展，以保持其正确性，并使其可能处理的CPU密集型任务，如证据检查的SAT痕迹。
Coqhas 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.