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.
This work was supported in part by the french ANR DECERT initiative.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baker, H.G.: Shallow Binding Makes Functional Arrays Fast. ACM SIGPLAN notices 26, 145–147 (1991)
Barras, B., Grégoire, B.: On the Role of Type Decorations in the Calculus of Inductive Constructions. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 151–166. Springer, Heidelberg (2005)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)
Boyer, R.S., Moore, J.S.: Single-Threaded Objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, pp. 9–27. Springer, Heidelberg (2002)
Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative Functional Programming with Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008)
Conchon, S., Filliâtre, J.-C.: A persistent union-find data structure. In: ACM Workshop on ML, pp. 37–46 (2007)
Darbari, A., Fischer, B., Marques-Silva, J.: Formalizing a SAT Proof Checker in Coq. First Coq Workshop, published as technical report tum-i0919 of the Technical University of Munich (2009)
Gonthier, G.: Formal Proof – The Four-Color Theorem. Notices of the AMS 55(11) (2008)
Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP, pp. 235–246 (2002)
Kroening, D., Strichman, O.: Decision Procedures, An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer, Heidelberg (2008)
Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA (1990)
Leroy, X.: Objective Caml (1997), http://ocaml.inria.fr/
Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)
Shankar, N.: Static Analysis for Safe Destructive Updates in a Functional Language. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol. 2372, pp. 1–24. Springer, Heidelberg (2002)
Swierstra, W.: A Hoare Logic for the State Monad. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 440–451. Springer, Heidelberg (2009)
Théry, L.: Proof Pearl: Revisiting the Mini-Rubik in Coq. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 310–319. Springer, Heidelberg (2008)
Princeton University. zChaff, http://www.princeton.edu/~chaff/zchaff.html
Wadler, P.: Monads for Functional Programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995)
Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. Applied Logic 7(1), 26–40 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armand, M., Grégoire, B., Spiwack, A., Théry, L. (2010). Extending Coq with Imperative Features and Its Application to SAT Verification. In: Kaufmann, M., Paulson, L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-14052-5_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14051-8
Online ISBN: 978-3-642-14052-5
eBook Packages: Computer ScienceComputer Science (R0)