/me reviewed section 3, here I go ...

[helm.git] / helm / papers / matita / matita2.bbl

diff --git a/helm/papers/matita/matita2.bbl b/helm/papers/matita/matita2.bbl
index 03704995b8785b2392e8368c9a46ab90b1c565b5..c3dd6c1884b97c175c106e155b0a43417d937601 100644 (file)
--- a/helm/papers/matita/matita2.bbl
+++ b/helm/papers/matita/matita2.bbl
@@ -44,15 +44,21 @@ Aspinall, D.: 2000, `{P}roof {G}eneral: A Generic Tool for Proof Development'.
 Barthe, G.: 1995, `Implicit Coercions in Type Systems'.
 \newblock In: {\em {TYPES}}. pp. 1--15.
 
-\bibitem{proof-by-pointing}
-Bertot, Y.: 1993, `Proof by Pointing'.
-\newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)},
-  Vol. 789 of {\em Lecture Notes in Computer Science}.
-
 \bibitem{ctcoq1}
 Bertot, Y.: 1999, `The CtCoq System: Design and Architecture'.
 \newblock {\em Formal Aspects of Computing} {\bf 11}, 225--243.
 
+\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éry: 1994, `Proof by Pointing'.
+\newblock In: {\em Symposium on Theoretical Aspects Computer Software (STACS)},
+  Vol. 789 of {\em Lecture Notes in Computer Science}.
+
 \bibitem{gdome2}
 Casarini, P. and L. Padovani: 2002, `The {G}nome {DOM} {E}ngine'.
 \newblock {\em Markup Languages: Theory \& Practice} {\bf 3}(2), 173--190.
@@ -90,9 +96,9 @@ MathML: 2003, `Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0'.
   \url{http://www.w3.org/TR/MathML2}.
 
 \bibitem{paramodulation}
-Nieuwenhuis, R. and A. Rubio: 2001, `Paramodulation-based thorem proving'.
-\newblock In: J.~A. Robinson and A. Voronkov (eds.): {\em Handbook of Automated
-  Reasoning}. pp. 471--443.
+Nieuwenhuis, R. and A. Rubio: 2001, {\em Paramodulation-based thorem proving}.
+\newblock Elsevier and MIT Press.
+\newblock ISBN-0-262-18223-8.
 
 \bibitem{omdoc}
 OMDoc: 2005, `{OMDoc}: An Open Markup Format for Mathematical Documents