J. R. , The B-Book. Assigning programs to meaning. C a m bridge University Press, 1996.

K. R. Apt and E. Olderog, Veriication of sequential and concurrent programs, 1991.

B. Barras, S. Boutin, C. Cornes, J. Courant, J. Filli^-atre et al., The Coq P r oof Assistant Reference Manual Version 6, 1996.

T. Coquand and G. Huet, The Calculus of Constructions. Information and Computation, vol.76, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00076024

J. Filli^-atre, Functional translation of imperative programs

J. Girard, Y. Lafont, and P. , Proofs and Types, 1989.

I. Hayes, Speciication Case Studies, 1985.

C. A. Hoare, An axiomatic basis for computer programming, 576{580,583, vol.12, 1969.

C. B. Jones, Systematic Software Development using VDM, 1989.

S. C. Kleene, Introduction to Metamathematics. Bibliotheca Mathematica, 1952.

P. W. O'hearn and J. C. Reynolds, From Algol to Polymorphic Linear Lambda-calculus, 1997.

C. Parent, Developing certiied programs in the system Coq { The Program tactic, Proceedings of the BRA Workshop Types for Proofs and Programs, vol.9, p.3, 1993.

C. Paulin-mohring, Extracting F ! 's programs from proofs in the Calculus of Constructions, Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989.

C. Paulin-mohring, Proceedings of the conference T yped L ambda Calculi and Applications, n umber 664 in LNCS, 1993. Also LIP research report, pp.92-141

W. Reif, The KIV-approach t o S o f t ware Veriication, KORSO: Methods, Languages, and Tools for the Construction of Correct Software { Final Report. Springer LNCS 1009, 1995.

T. Schreiber, Auxiliary variables and recursive procedures, TAPSOFT'97: Theory and Practice of Software Development, v olume 1214 of Lecture Notes in Computer Science, pp.697-711, 1997.