Skip to main content
SpringerLink
Log in

From Sets to Bits in Coq

  • Conference paper
  • First Online:
Functional and Logic Programming (FLOPS 2016)

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

Included in the following conference series:

Abstract

Computer Science abounds in folktales about how — in the early days of computer programming — bit vectors were ingeniously used to encode and manipulate finite sets. Algorithms have thus been developed to minimize memory footprint and maximize efficiency by taking advantage of microarchitectural features. With the development of automated and interactive theorem provers, finite sets have also made their way into the libraries of formalized mathematics. Tailored to ease proving, these representations are designed for symbolic manipulation rather than computational efficiency. This paper aims to bridge this gap. In the Coq proof assistant, we implement a bitset library and prove its correctness with respect to a formalization of finite sets. Our library enables a seamless interaction of sets for computing — bitsets — and sets for proving — finite sets.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Notes

  1. 1.

    Needless to say, this example is drawn from the authors’ harsh experience.

  2. 2.

    Boolean values are transparently lifted to types through the predicate that assigns the empty set to and the unit set otherwise.

References

  1. Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

    Book  MATH  Google Scholar 

  2. Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Symposium on Logic in Computer Science (LICS 1990), pp. 95–105 (1990)

    Google Scholar 

  3. Beeler, M., Gosper, R.W., Schroeppel, R.: Hakmem. Tech. report Massachusetts Institute of Technology (1972). http://hdl.handle.net/1721.1/6086

  4. Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422–426 (1970)

    Article  MATH  Google Scholar 

  5. Bobot, F., Filliâtre, J.C., Marché, C., Melquiond, G., Paskevich, A.: The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay (2015)

    Google Scholar 

  6. Charguéraud, A.: Characteristic formulae for the verification of imperative programs. In: International Conference on Functional programming (ICFP 2011), pp. 418–430 (2011)

    Google Scholar 

  7. Klein, G., Cock, D., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167–182. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Cohen, C., Dénès, M., Mörtberg, A.: Refinements for free!. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 147–162. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Coq Standard Library: Finite sets. https://coq.inria.fr/library/Coq.Sets.Finite_sets.html

  10. Coq Standard Library: Modular implementation of finite sets. https://coq.inria.fr/library/Coq.MSets.MSets.html

  11. Delaware, B., Pit-Claudel, C., Gross, J., Chlipala, A.: Fiat: deductive synthesis of abstract data types in a proof assistant. In: Principles of Programming Languages (POPL 2015), pp. 689–700 (2015)

    Google Scholar 

  12. Dénès, M., Mörtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 83–98. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Filliâtre, J.-C.: Verifying two lines of C with Why3: an exercise in program verification. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 83–97. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243–258. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. Technical report RR-6455, INRIA (2008)

    Google Scholar 

  16. Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  17. Hedberg, M.: A coherence theorem for Martin-Löf’s type theory. J. Funct. Program. 8(4), 413–436 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  18. Kennedy, A., Benton, N., Jensen, J.B., Dagand, P.E.: Coq: The world’s best macro assembler? In: Symposium on Principles and Practice of Declarative Programming (PPDP 2013), pp. 13–24 (2013)

    Google Scholar 

  19. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  20. Mathematical Components: Finite sets. http://ssr2.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.finset.html

  21. Mérillon, F., Réveillère, L., Consel, C., Marlet, R., Muller, G.: Devil: an IDL for hardware programming. In: Symposium on Operating Systems Design and Implementation (OSDI 2000) (2000)

    Google Scholar 

  22. Necula, G.C.: Translation validation for an optimizing compiler. In: Conference on Programming Language Design and Implementation (PLDI 2000), pp. 83–94 (2000)

    Google Scholar 

  23. OCaml Standard Library: Pervasives. http://caml.inria.fr/pub/docs/manual-ocaml/libref/Pervasives.html

  24. Richards, M.: Backtracking algorithms in MCPL using bit patterns and recursion (1997)

    Google Scholar 

  25. Ssreflect library: Finite type. http://ssr.msr-inria.inria.fr/doc/ssreflect-1.5/Ssreflect.fintype.html

  26. Ssreflect library: Tuple. http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.tuple.html

  27. Warren, H.S.: Hacker’s Delight. Addison-Wesley Professional, Boston (2012)

    Google Scholar 

Download references

Acknowledgements

We are grateful to Arthur Charguéraud and Maxime Dénès for several discussions on these questions. We also thank Jean-Christophe Filliâtre for suggesting the n-queens example, and Clément Fumex and Claude Marché for pointers to the literature. We finally thank the anonymous FLOPS reviewers, whose remarks helped us to streamline our presentation.

Author information

Authors and Affiliations

  1. Sorbonne Universités, UPMC Univ Paris 06, CNRS, Inria, LIP6 UMR 7606, Paris, France

    Arthur Blot, Pierre-Évariste Dagand & Julia Lawall

Authors
  1. Arthur Blot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierre-Évariste Dagand
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Julia Lawall
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Arthur Blot .

Editor information

Editors and Affiliations

  1. Tohoku University, Sendai, Japan

    Oleg Kiselyov

  2. School of Computing, University of Kent, Canterbury, United Kingdom

    Andy King

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Blot, A., Dagand, PÉ., Lawall, J. (2016). From Sets to Bits in Coq. In: Kiselyov, O., King, A. (eds) Functional and Logic Programming. FLOPS 2016. Lecture Notes in Computer Science(), vol 9613. Springer, Cham. https://doi.org/10.1007/978-3-319-29604-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29604-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29603-6

  • Online ISBN: 978-3-319-29604-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation