diff -r 50838e25f73c -r d14b8b21bef2 Paper/document/root.bib
--- a/Paper/document/root.bib	Fri Mar 19 15:43:59 2010 +0100
+++ b/Paper/document/root.bib	Fri Mar 19 17:20:25 2010 +0100
@@ -11,8 +11,7 @@
 @InProceedings{Homeier05,
   author = 	 {P.~Homeier},
   title = 	 {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients},
-  booktitle = 	 {Proc.~of the 18th International Conference on Theorem 
-                  Proving in Higher Order Logics (TPHOLs)},
+  booktitle = 	 {Proc.~of the 18th TPHOLs Conference},
   pages = 	 {130--146},
   year = 	 {2005},
   volume = 	 {3603},
@@ -28,7 +27,7 @@
                S.~Sarkar and 
                R.~Strni\v{s}a},
  title      = {{Ott}: {E}ffective {T}ool {S}upport for the {W}orking {S}emanticist},
- journal    = {Journal of Functional Programming},
+ journal    = {J.~of Functional Programming},
  year       = {2010},
  volume     = {20},
  number     = {1},
@@ -49,7 +48,7 @@
 @Unpublished{HuffmanUrban10,
   author = 	 {B.~Huffman and C.~Urban},
   title = 	 {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
-  note = 	 {To appear at ITP 2010},
+  note = 	 {To appear at {\it ITP'10 Conference}},
   annote =       {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
   year = 	 {2010}
 }
@@ -75,8 +74,7 @@
                   S.~Zdancewic},
   title = 	 {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark 
                   {C}hallenge},
-  booktitle = 	 {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order 
-                  Logics (TPHOLs)},
+  booktitle = 	 {Proc.~of the 18th TPHOLs Conference},
   pages = 	 {50--65},
   year = 	 {2005},
   volume = 	 {3603},
@@ -86,7 +84,7 @@
 @Unpublished{SatoPollack10,
   author = 	 {M.~Sato and R.~Pollack},
   title = 	 {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},
-  note = 	 {To appear in {\it Journal of Symbolic Computation}}
+  note = 	 {To appear in {\it J.~of Symbolic Computation}}
 }
 
 @article{GabbayPitts02,
@@ -112,8 +110,7 @@
 @InProceedings{BengtsonParrow07,
   author    = {J.~Bengtson and J.~Parrow},
   title     = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
-  booktitle = {Proc.~of the 10th International Conference on
-               Foundations of Software Science and Computation Structures (FOSSACS)},
+  booktitle = {Proc.~of the 10th FOSSACS Conference},
   year      = 2007,
   pages     = {63--77},
   series    = {LNCS},
@@ -123,8 +120,7 @@
 @inproceedings{BengtsonParow09,
   author    = {J.~Bengtson and J.~Parrow},
   title     = {{P}si-{C}alculi in {I}sabelle},
-  booktitle = {Proc of the 22nd Conference on Theorem Proving in 
-               Higher Order Logics (TPHOLs)},
+  booktitle = {Proc of the 22nd TPHOLs Conference},
   year      = 2009,
   pages     = {99--114},
   series    = {LNCS},
@@ -133,8 +129,7 @@
 
 @inproceedings{TobinHochstadtFelleisen08,
   author    = {S.~Tobin-Hochstadt and M.~Felleisen},
-  booktitle = {Proc.~of the 35rd Symposium on
-               Principles of Programming Languages (POPL)},
+  booktitle = {Proc.~of the 35rd POPL Symposium},
   title     = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
   publisher = {ACM},
   year      = {2008},
@@ -146,14 +141,13 @@
   title = "{M}echanizing the {M}etatheory of {LF}",
   pages = "45--56",
   year = 2008,
-  booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)"
+  booktitle = "Proc.~of the 23rd LICS Symposium"
 }
 
 @InProceedings{UrbanZhu08,
   title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof",
   author = "C.~Urban and B.~Zhu",
-  booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques 
-                     and Applications (RTA)",
+  booktitle = "Proc.~of the 9th RTA Conference",
   year = "2008",
   pages = "409--424",
   series = "LNCS",