+@book{CoqArt,
+ author = "Yves Bertot and Pierre Castéran",
+ title = "{Interactive Theorem Proving and Program Development}",
+ publisher = {Springer Verlag},
+ series = {Texts in Theoretical Computer Science},
+ year = 2004,
+ NOTE = {ISBN-3-540-20854-2}
+
+}
+