Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2010: Interactive Theorem Proving pp 83–98Cite as

Extending Coq with Imperative Features and Its Application to SAT Verification

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6172))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baker, H.G.: Shallow Binding Makes Functional Arrays Fast. ACM SIGPLAN notices 26, 145–147 (1991)

    Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. 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)

    MATH  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Conchon, S., Filliâtre, J.-C.: A persistent union-find data structure. In: ACM Workshop on ML, pp. 37–46 (2007)

    Google Scholar 

  7. 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)

    Google Scholar 

  8. Gonthier, G.: Formal Proof – The Four-Color Theorem. Notices of the AMS 55(11) (2008)

    Google Scholar 

  9. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP, pp. 235–246 (2002)

    Google Scholar 

  10. Kroening, D., Strichman, O.: Decision Procedures, An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  11. Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA (1990)

    Google Scholar 

  12. Leroy, X.: Objective Caml (1997), http://ocaml.inria.fr/

  13. Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)

    Book  Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Swierstra, W.: A Hoare Logic for the State Monad. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 440–451. Springer, Heidelberg (2009)

    Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Princeton University. zChaff, http://www.princeton.edu/~chaff/zchaff.html

  18. Wadler, P.: Monads for Functional Programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995)

    Google Scholar 

  19. Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. J. Applied Logic 7(1), 26–40 (2009)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia Antipolis - Méditerranée, France

    Michaël Armand, Benjamin Grégoire & Laurent Théry

  2. LIX, École Polytechnique, France

    Arnaud Spiwack

Authors
  1. Michaël Armand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benjamin Grégoire
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Arnaud Spiwack
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Sciences, University of Texas, Austin, Talyor Hall 2.124, 78712-1188, Austin, TX, USA

    Matt Kaufmann

  2. Computer Laboratory, University of Cambridge, CB3 0FD, Cambridge,, UK

    Lawrence C. Paulson

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation