Skip to main content
SpringerLink
Log in

Proof of Imperative Programs in Type Theory

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 1998)

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

Included in the following conference series:

Abstract

We present a new approach to certifying functional programs with imperative aspects, in the context of Type Theory. The key is a functional translation of imperative programs, based on a combination of the type and effect discipline and monads. Then an incomplete proof of the specification is built in the Type Theory, whose gaps would correspond to proof obligations. On sequential imperative programs, we get the same proof obligations as those given by Floyd-Hoare logic. Compared to the latter, our approach also includes functional constructions in a straight-forward way. This work has been implemented in the Coq Proof Assistant and applied on non-trivial examples.

This research was partly supported by ESPRIT Working Group “Types”.

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. The Coq Proof Assistant. http://coq.inria.fr/. 78, 80, 90

  2. J. R. Abrial. The B-Book. Assigning programs to meaning. Cambridge University Press, 1996. 78, 91

    Google Scholar 

  3. P. Chartier. Formalization of B in Isabelle/HOL. In Proceedings of the Second B International Conference, Montepellier, France, April 1998. Springer Verlag LNCS 1393. 91

    Google Scholar 

  4. P. Cousot. Handbook of Theoretical Computer Science, volume B, chapter Methods and Logics for Proving Programs, pages 841–993. Elsevier Science Publishers B. V., 1990. 78, 79, 90

    MathSciNet  Google Scholar 

  5. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976. 78

    Google Scholar 

  6. R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, Proceedings of Symposia in applied Mathematics 19, pages 19–32, Providence, 1967. American Mathematical Society. 78

    Google Scholar 

  7. Mike Gordon. Teaching and Learning Formal Methods, chapter Teaching hardware and software verification in a uniform framework. Academic Press, 1996. 78, 91

    Google Scholar 

  8. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580,583, 1969. Also in [10] 45-58. 78

    Article  MATH  Google Scholar 

  9. C. A. R. Hoare. Proof of a program: Find. Communications of the ACM, 14(1):39–45, January 1971. Also in [10] 59–74. 91

    Article  MATH  Google Scholar 

  10. C. A. R. Hoare and C. B. Jones. Essays in Computing Science. Prentice Hall, New York, 1989. 92

    MATH  Google Scholar 

  11. E. Moggi. Computational lambda-calculus and monads. In IEEE Symposium on Logic in Computer Science, 1989. 79, 81

    Google Scholar 

  12. C. Muñoz. Supporting the B-method in PVS: An Approach to the Abstract Machine Notation in Type Theory. Submitted to FSE-98, 1998. 91

    Google Scholar 

  13. C. Parent. Developing certified programs in the system Coq-The Program tactic. Technical Report 93-29, Ecole Normale Supérieure de Lyon, October 1993. Also in Proceedings of the BRA Workshop Types for Proofs and Programs, May 93. 79

    Google Scholar 

  14. C. Paulin-Mohring. Extracting Fω’s programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM. 87, 89

    Google Scholar 

  15. T. Schreiber. Auxiliary variables and recursive procedures. In TAPSOFT’97: Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 697–711. Springer-Verlag, April 1997. 78, 90, 91

    Chapter  Google Scholar 

  16. J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111(2):245–296, 1994. 79, 80

    Article  MATH  MathSciNet  Google Scholar 

  17. P. Wadler. Monads for functional programming. In Proceedings of the Marktoberdorf Summer School on Program Design Calculi, August 1992. 79, 81

    Google Scholar 

  18. A. K. Wright and M. Felleisen. A Syntactic Approach to Type Soundness. Information and Computation, 115:38–94, 1994. 85

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRI, URA CNRS 410, Bât. 490, Université Paris Sud, 91405, ORSAY Cedex, France

    Jean-Christophe Filliâtre

Authors
  1. Jean-Christophe Filliâtre
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Ludwig-Maximilians-Universität, Institut für Informatik, Oettingenstr. 67, D-80538, München, Germany

    Thorsten Altenkirch  & Bernhard Reus  & 

  2. Technische Universität München, Institut für Informatik, Arcisstr. 21-1528, D-80290, München, Germany

    Wolfgang Naraschewski

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Filliâtre, JC. (1999). Proof of Imperative Programs in Type Theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-48167-2_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66537-3

  • Online ISBN: 978-3-540-48167-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation