--- a/Journal/document/root.bib	Thu Aug 25 19:33:41 2011 +0000
+++ b/Journal/document/root.bib	Fri Aug 26 17:23:46 2011 +0000
@@ -1,5 +1,15 @@
 
-
+@incollection{myhillnerodeafp11,
+  author =       {C.~Wu and X.~Zhang and C.~Urban},
+  title =        {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
+  booktitle =    {The Archive of Formal Proofs},
+  editor =       {G.~Klein and T.~Nipkow and L.~Paulson},
+  publisher =    {\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}},
+  month =        Aug,
+  year =         2011,
+  note =         {Formal proof development},
+  ISSN =         {2150-914x}
+}
 
 @PhdThesis{Haftmann09,
   author = 	 {F.~Haftmann},
@@ -63,6 +73,18 @@
 }
 
 
+
+@InProceedings{Almeidaetal10,
+  author =       {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},
+  title =        {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},
+  booktitle =    {Proc.~of the 15th International Conference on Implementation
+                  and Application of Automata},
+  pages =        {59-68},
+  year =         {2010},
+  volume =       {6482},
+  series =       {LNCS}
+}
+
 @incollection{Constable00,
   author    = {R.~L.~Constable and
                P.~B.~Jackson and