Proof of Imperative Programs in Type Theory

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