--- a/Quotient-Paper/document/root.bib	Fri Oct 29 14:25:50 2010 +0900
+++ b/Quotient-Paper/document/root.bib	Fri Oct 29 15:37:24 2010 +0100
@@ -1,13 +1,13 @@
 @inproceedings{Nogin02,
   author    = {Aleksey Nogin},
   title     = {Quotient Types: A Modular Approach},
-  booktitle = {TPHOLs},
+  booktitle = {Proc.~of the 15th TPHOLs conference},
   year      = {2002},
   pages     = {263-280},
-  ee        = {http://link.springer.de/link/service/series/0558/bibs/2410/24100263.htm},
-  crossref  = {DBLP:conf/tphol/2002},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {2646}
 }
+
 @proceedings{DBLP:conf/tphol/2002,
   editor    = {Victor Carre{\~n}o and
                C{\'e}sar Mu{\~n}oz and
@@ -38,12 +38,11 @@
                Loic Pottier and
                Carlos Simpson},
   title     = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq},
-  booktitle = {TYPES},
+  booktitle = {Proc of the TYPES workshop},
   year      = {2002},
   pages     = {95-107},
-  ee        = {http://link.springer.de/link/service/series/0558/bibs/2646/26460095.htm},
-  crossref  = {DBLP:conf/types/2002},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {2646}
 }
 
 @proceedings{DBLP:conf/types/2002,
@@ -77,13 +76,13 @@
   author    = {Oscar Slotosch},
   title     = {Higher Order Quotients and their Implementation in Isabelle
                HOL},
-  booktitle = {TPHOLs},
+  booktitle = {Proc.~of the 10th TPHOLs conference},
   year      = {1997},
   pages     = {291-306},
-  ee        = {http://dx.doi.org/10.1007/BFb0028401},
-  crossref  = {DBLP:conf/tphol/1997},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {1275}
 }
+
 @proceedings{DBLP:conf/tphol/1997,
   editor    = {Elsa L. Gunter and
                Amy P. Felty},
@@ -102,13 +101,13 @@
 @inproceedings{Homeier05,
   author    = {Peter V. Homeier},
   title     = {A Design Structure for Higher Order Quotients},
-  booktitle = {TPHOLs},
+  booktitle = {Proc of the 18th TPHOLs conference},
   year      = {2005},
   pages     = {130-146},
-  ee        = {http://dx.doi.org/10.1007/11541868_9},
-  crossref  = {DBLP:conf/tphol/2005},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  series    = {LNCS},
+  volume    = {3603}
 }
+
 @proceedings{DBLP:conf/tphol/2005,
   editor    = {Joe Hurd and
                Thomas F. Melham},