+\bibitem{CoqArt}
+Bertot, Y. and P. Castéran: 2004, {\em {Interactive Theorem Proving and
+ Program Development}}, Texts in Theoretical Computer Science.
+\newblock Springer Verlag.
+\newblock ISBN-3-540-20854-2.
+
+\bibitem{proof-by-pointing}
+Bertot, Y., G. Kahn, and L. Th\'ery: 1994, `Proof by Pointing'.
+\newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)},
+ Vol. 789 of {\em Lecture Notes in Computer Science}.
+