Skip to main content
SpringerLink
Log in

Efficient Reasoning about Executable Specifications in Coq

  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2410))

Included in the following conference series:

Abstract

We describe a package to reason efficiently about executable specifications in Coq. The package provides a command for synthesizing a customized induction principle for a recursively defined function, and a tactic that combines the application of the customized induction principle with automatic rewriting. We further illustrate how the package leads to a drastic reduction (by a factor of 10 approximately) of the size of the proofs in a large-scale case study on reasoning about JavaCard.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. C. Alvarado and Q.-H. Nguyen, elan for equational reasoning in coq. In J. Despeyroux, editor, Proceedings of LFM’OO, 2000. Rapport Technique INRIA.

    Google Scholar 

  2. G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In I. Attali and T. Jensen, editors, Proceedings of e-SMART 2001, volume 2140 of Lecture Notes in Computer Science, pages 2–18. Springer-Verlag, 2001.

    Google Scholar 

  3. G. Barthe, G. Dufay, L. Jakubiec, and S. Melo de Sousa. A formal correspondence between offensive and defensive JavaCard virtual machines. In A. Cortesi, editor, Proceedings of VMCAI 2002, volume 2294 of Lecture Notes in Computer Science, pages 32–45. Springer-Verlag, 2002.

    Google Scholar 

  4. G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP 2001, volume 2028 of Lecture Notes in Computer Science, pages 302–319. Springer-Verlag, 2001.

    Google Scholar 

  5. S. Berghofer and T. Nipkow. Executing higher order logic. In P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, editors, Proceedings of TYPES 2000, volume LNCS 2277 of Lecture Notes in Computer Science. Springer-Verlag, 2002.

    Chapter  Google Scholar 

  6. P. Borovanský, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, and M. Vittek. The Elan VS.4. Manual, 2000.

    Google Scholar 

  7. A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23:47–77, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  8. R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988.

    Google Scholar 

  9. Coq Development Team. The Coq Proof Assistant User’s Guide. Version 1.2, January 2002.

    Google Scholar 

  10. C. Cornes. Conception d’un langage de haut niveau de representation de preuves: Récurrence par filtrage de motifs; Unification en présence de types inductifs primitifs; Synthèse de lemmes d’inversion. PhD thesis, Université de Paris 7, 1997.

    Google Scholar 

  11. C. Cornes and D. Terrasse. Automating inversion and inductive predicates in Coq. In S. Berardi and M. Coppo, editors, Proceedings of Types’95, volume 1158 of Lecture Notes in Computer Science, pages 85–104. Springer-Verlag, 1995.

    Google Scholar 

  12. P. Courtieu. Function Schemes in Coq: Documentation and tutorial. See http://www-sop.inria.fr/lemme/Pierre.Courtieu/funscheme.html

  13. M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL: A theorem proving environment for higher-order logic. Cambridge University Press, 1993.

    Google Scholar 

  14. J.-L. Lanet and A. Requet. Formal Proof of Smart Card Applets Correctness. In J.-J. Quisquater and B. Schneier, editors, Proceedings of CARDIS’98, volume 1820 of Lecture Notes in Computer Science, pages 85–97. Springer-Verlag, 1998.

    Google Scholar 

  15. Z. Luo and R. Pollack. LEGO proof development system: User’s manual. Technical Report ECS-LFCS-92-211, LFCS, University of Edinburgh, May 1992.

    Google Scholar 

  16. C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA’ 93, volume 664 of Lecture Notes in Computer Science, pages 328–345. Springer-Verlag, 1993.

    Google Scholar 

  17. C. Paulin-Mohring. Définitions Inductives en Theorie des Types d’Ordre Superieur. Habilitation à diriger les recherches, Université Claude Bernard Lyon I, 1996.

    Google Scholar 

  18. L. Paulson. Isabelle: A generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

    MATH  Google Scholar 

  19. F. Pfenning. Elf: a meta-language for deductive systems. In A. Bundy, editor, Proceedings of CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 811–815. Springer-Verlag, 1994.

    Google Scholar 

  20. K. Slind. Reasoning about Terminating Functional Programs. PhD thesis, TU Münich, 1999.

    Google Scholar 

  21. D. Terrasse. Encoding natural semantics in Coq. In V. S. Alagar, editor, Proceedings of AMAST’95, volume 936 of Lecture Notes in Computer Science, pages 230–244. Springer-Verlag, 1995.

    Google Scholar 

  22. D. Terrasse. Vers un environnement d’aide au développement de preuves en Sémantique Naturelle. PhD thesis, Ecole Nationale des Ponts et Chaussées, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, Sophia-Antipolis, France

    Gilles Barthe & Pierre Courtieu

Authors
  1. Gilles Barthe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pierre Courtieu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, MS 130, Hampton, VA, 23681, USA

    Victor A. Carreño

  2. ICASE-Langley Research Center, MS 132C, Hampton, VA, 23681, USA

    César A. Muñoz

  3. Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve Blvd.W., Montréal, Québec, H3G 1M8, Canada

    Sofiène Tahar

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Barthe, G., Courtieu, P. (2002). Efficient Reasoning about Executable Specifications in Coq. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2002. Lecture Notes in Computer Science, vol 2410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45685-6_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-45685-6_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44039-0

  • Online ISBN: 978-3-540-45685-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation