+\bibitem{delahaye}
+Delahaye, D. and R. di~Cosmo: 1999, `Information Retrieval in a {C}oq Proof
+ Library using Type Isomorphisms'.
+\newblock In: {\em Proceedings of TYPES 99}, Vol. LNCS.
+
+\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 In: {\em Lecture Notes in Computer Science}, Vol.~78 of {\em Lecture
+ Notes in Computer Science}.
+
+\bibitem{lego}
+Lego, `The {L}ego proof-assistant'.
+\newblock \\\url{http://www.dcs.ed.ac.uk/home/lego/}.
+