--- a/Paper/document/root.bib	Sat Mar 05 11:06:39 2011 +0000
+++ b/Paper/document/root.bib	Sat Mar 05 11:42:14 2011 +0000
@@ -25,7 +25,7 @@
 }
 
 
-@inproceedings{Constable00,
+@incollection{Constable00,
   author    = {R.~L.~Constable and
                P.~B.~Jackson and
                P.~Naumov and
@@ -33,6 +33,7 @@
   title     = {{C}onstructively {F}ormalizing {A}utomata {T}heory},
   booktitle = {Proof, Language, and Interaction},
   year      = {2000},
+  publisher = {MIT Press},
   pages     = {213-238}
 }
 
@@ -81,9 +82,9 @@
 @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)},
+  booktitle={Proc.~of the International Workshop on Types for Proofs and Programs},
   year=2002,
-  series=LNCS,
+  series={LNCS},
   volume=2277,
   pages="24--40"
 }
@@ -105,6 +106,6 @@
                Conference on Theorem Proving in Higher Order Logics},
   year      = {2009},
   pages     = {147-163},
-  series    = LNCS,
+  series    = {LNCS},
   volume    = {5674}
 }
\ No newline at end of file