--- a/Paper/document/root.bib	Mon Feb 14 07:42:16 2011 +0000
+++ b/Paper/document/root.bib	Mon Feb 14 09:38:18 2011 +0000
@@ -1,3 +1,10 @@
+
+@Unpublished{KraussNipkow11,
+  author = 	 {A.~Kraus and T.~Nipkow},
+  title = 	 {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+  note = 	 {To appear in Journal of Automated Reasoning},
+  year = 	 {2011}
+}
 
 @Book{Kozen97,
   author = 	 {D.~Kozen},
@@ -58,4 +65,14 @@
  volume=1479,
  pages={1--15},
  year=1998
+}
+
+@inproceedings{BerghoferNipkow00,
+  author={S.~Berghofer and T.~Nipkow},
+  title={{E}xecuting {H}igher {O}rder {L}ogic},
+  booktitle={Types for Proofs and Programs (TYPES 2000)},
+  year=2002,
+  series=LNCS,
+  volume=2277,
+  pages="24--40"
 }
\ No newline at end of file