--- a/Journal/document/root.bib	Mon Oct 15 13:23:52 2012 +0000
+++ b/Journal/document/root.bib	Mon Dec 03 08:16:58 2012 +0000
@@ -1,4 +1,32 @@
+@InProceedings{CoquandSiles12,
+  author =       {T.~Coquand and V.~Siles},
+  title =        {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
+  booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs},
+  pages =     {119--134},
+  year =      {2011},
+  volume =    {7086},
+  series =    {LNCS}
+}
 
+@InProceedings{Asperti12,
+  author =       {A.~Asperti},
+  title =        {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
+  booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+  pages =     {283--298},
+  year =      {2012},
+  volume =    {7406},
+  series =    {LNCS}
+}
+
+@InProceedings{LammichTuerk12,
+  author =       {P.~Lammich and T.~Tuerk},
+  title =        {{A}pplying {D}ata {R}efinement for {M}onadic {P}rograms to {H}opcroft's {A}lgorithm},
+  booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+  year =      {2012},
+  volume =    {7406},
+  series =    {LNCS},
+  pages = {166--182}
+}
 
 @PhdThesis{Braibant12,
   author =       {T.~Braibant},
@@ -120,11 +148,14 @@
 
 
 
-@Unpublished{KraussNipkow11,
+@article{KraussNipkow11,
   author = 	 {A.~Krauss and T.~Nipkow},
   title = 	 {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
-  note = 	 {To appear in the Journal of Automated Reasoning},
-  year = 	 {2012}
+  journal = {Journal of Automated Reasoning},
+  volume = 49,
+  number = {1},
+  year = 	 {2012},
+  pages = {95--106}
 }
 
 @Book{Kozen97,