Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2013: Interactive Theorem Proving pp 180–196Cite as

Kleene Algebra with Tests and Coq Tools for while Programs

  • Conference paper

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

Abstract

We present a Coq library about Kleene algebra with tests, including a proof of their completeness over the appropriate notion of languages, a decision procedure for their equational theory, and tools for exploiting hypotheses of a certain kind in such a theory.

Kleene algebra with tests make it possible to represent if-then-else statements and while loops in imperative programming languages. They were actually introduced as an alternative to propositional Hoare logic.

We show how to exploit the corresponding Coq tools in the context of program verification by proving equivalences of while programs, correctness of some standard compiler optimisations, Hoare rules for partial correctness, and a particularly challenging equivalence of flowchart schemes.

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   39.99
Price excludes VAT (USA)
  • Available as 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Proc. LICS, pp. 95–105. IEEE Computer Society (1990)

    Google Scholar 

  2. Almeida, J.B., Moreira, N., Pereira, D., de Sousa, S.M.: Partial derivative automata formalized in Coq. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol. 6482, pp. 59–68. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. Angus, A., Kozen, D.: Kleene algebra with tests and program schematology. Technical Report TR2001-1844, CS Dpt, Cornell University (July 2001)

    Google Scholar 

  4. Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. TCS 155(2), 291–319 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  5. Armstrong, A., Struth, G.: Automated reasoning in higher-order regular algebra. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 66–81. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Asperti, A.: A compact proof of decidability for regular expression equivalence. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 283–298. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Boyer, R., Moore, J.: Metafunctions: proving them correct and using them efficiently as new proof procedures. In: The Correctness Problem in Computer Science. Academic Press, NY (1981)

    Google Scholar 

  9. Braibant, T., Pous, D.: An efficient Coq tactic for deciding Kleene algebras. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 163–178. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)

    Article  MathSciNet  MATH  Google Scholar 

  11. Cohen, E.: Hypotheses in Kleene algebra. Technical report, Bellcore, Morristown, N.J (1994)

    Google Scholar 

  12. Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 119–134. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Foster, S., Struth, G.: Automated analysis of regular algebra. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 271–285. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  14. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Hardin, C., Kozen, D.: On the elimination of hypotheses in Kleene algebra with tests. Technical Report TR2002-1879, CS Dpt, Cornell University (October 2002)

    Google Scholar 

  16. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  17. Komendantsky, V.: Reflexive toolbox for regular expression matching: verification of functional programs in Coq+ssreflect. In: Proc. PLPV, pp. 61–70. ACM (2012)

    Google Scholar 

  18. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. and Comp. 110(2), 366–390 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  19. Kozen, D.: Kleene algebra with tests. Transactions on Programming Languages and Systems 19(3), 427–443 (1997)

    Article  Google Scholar 

  20. Kozen, D.: Typed Kleene algebra, TR98-1669, CS Dpt. Cornell University (1998)

    Google Scholar 

  21. Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log. 1(1), 60–76 (2000)

    Article  MathSciNet  Google Scholar 

  22. Kozen, D.: On the coalgebraic theory of Kleene algebra with tests. Technical Report  CIS, Cornell University (March 2008), http://hdl.handle.net/1813/10173

  23. Kozen, D., Patron, M.-C.: Certification of compiler optimizations using Kleene algebra with tests. In: Palamidessi, C., et al. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 568–582. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  24. Kozen, D., Smith, F.: Kleene algebra with tests: Completeness and decidability. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244–259. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  25. Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. JAR 49(1), 95–106 (2012)

    Article  MathSciNet  Google Scholar 

  26. Manna, Z.: Mathematical Theory of Computation. McGraw-Hill (1974)

    Google Scholar 

  27. Moreira, N., Pereira, D., de Sousa, S.M.: Deciding regular expressions (In-) equivalence in Coq. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 98–113. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  28. Pereira, D., Moreira, N.: KAT and PHL in Coq. Comput. Sci. Inf. Syst. 5(2), 137–160 (2008)

    Article  Google Scholar 

  29. Pous, D.: Untyping typed algebraic structures and colouring proof nets of cyclic linear logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 484–498. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  30. Pous, D.: RelationAlgebra: Coq library containing all material presented in this paper (December 2012), http://perso.ens-lyon.fr/damien.pous/ra

  31. Thompson, K.: Regular expression search algorithm. C. ACM 11, 419–422 (1968)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS – LIP, ENS Lyon, UMR 5668, France

    Damien Pous

Authors
  1. Damien Pous
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IRISA, Université Rennes 1, Campus de Beaulieu, 35042, Rennes Cedex, France

    Sandrine Blazy

  2. Université Paris-Sud, LRI, Bat 650, Univ. Paris Sud, 91405, Orsay Cedex, France

    Christine Paulin-Mohring

  3. Inria Rennes-Bretagne Atlantique, Campus de Beaulieu, 35042, Rennes Cedex, France

    David Pichardie

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pous, D. (2013). Kleene Algebra with Tests and Coq Tools for while Programs. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds) Interactive Theorem Proving. ITP 2013. Lecture Notes in Computer Science, vol 7998. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39634-2_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39634-2_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39633-5

  • Online ISBN: 978-3-642-39634-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation