\bibitem{remathematization}
Asperti, A., L. Padovani, C. {Sacerdoti Coen}, and I. Schena: 2001, `{XML},
Stylesheets and the re-mathematization of Formal Content'.
-\newblock In: {\em EXTREME}.
+\newblock In: {\em Electronic Proceedings of {EXTREME Markup Languages} 2001}.
\bibitem{pechino}
Asperti, A. and B. Wegner: 2003, `An Approach to Machine-Understandable
\bibitem{barthe95implicit}
Barthe, G.: 1995, `Implicit Coercions in Type Systems'.
-\newblock In: {\em {TYPES}}. pp. 1--15.
+\newblock In: {\em Types for Proofs and Programs: International Workshop,
+ {TYPES 1995}}. pp. 1--15.
\bibitem{ctcoq1}
Bertot, Y.: 1999, `The CtCoq System: Design and Architecture'.
\newblock ISBN-3-540-20854-2.
\bibitem{proof-by-pointing}
-Bertot, Y., G. Kahn, and L. Théry: 1994, `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}.
\newblock Technical Report RR-2459, Inria (Institut National de Recherche en
Informatique et en Automatique), France.
+\bibitem{geuvers-jojgov}
+Geuvers, H. and G.~I. Jojgov: 2002, `Open Proofs and Open Terms: A Basis for
+ Interactive Logic'.
+\newblock In: J. Bradfield (ed.): {\em Computer Science Logic: 16th
+ International Workshop, CLS 2002}, Vol. LNCS, 2471. pp. 537--552.
+
\bibitem{lcf}
Gordon, M. J.~C., R. Milner, and C. Wadsworth: 1979, `{Edinburgh LCF}: a
Mechanised Logic of Computation'.
\newblock W3C Recommendation 21 February 2001,
\url{http://www.w3.org/TR/MathML2}.
+\bibitem{munoz}
+Munoz, C.: 1997, `A Calculus of Substitutions for Incomplete-Proof
+ Representation in Type Theory'.
+\newblock Ph.D. thesis, INRIA.
+
\bibitem{paramodulation}
Nieuwenhuis, R. and A. Rubio: 2001, {\em Paramodulation-based thorem proving}.
\newblock Elsevier and MIT Press.
\newblock In: A.~T. Andrea~Asperti, Grzegorz~Bancerek (ed.): {\em Proceedings
of Mathematical Knowledge Management 2004}, Vol. LNCS, 3119. pp. 347--362.
+\bibitem{strecker}
+Strecker, M.: 1998, `Construction and Deduction in Type Theories'.
+\newblock Ph.D. thesis, Universit{\"a}t Ulm.
+
\bibitem{CoqManual}
{The Coq Development Team}: 2005, `The {C}oq Proof Assistant Reference Manual'.
\newblock \\\url{http://coq.inria.fr/doc/main.html}.