--- a/Quotient-Paper/document/root.bib	Sun Jun 13 17:41:07 2010 +0200
+++ b/Quotient-Paper/document/root.bib	Sun Jun 13 20:54:50 2010 +0200
@@ -154,4 +154,51 @@
   note = 	 {submitted for publication},
   month =	 {July},
   year =	 {2010},
+}
+
+@InProceedings{BengtsonParrow07,
+  author    = {J.~Bengtson and J.~Parrow},
+  title     = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
+  booktitle = {Proc.~of the 10th FOSSACS Conference},
+  year      = 2007,
+  pages     = {63--77},
+  series    = {LNCS},
+  volume    = {4423}
+}
+
+@inproceedings{BengtsonParow09,
+  author    = {J.~Bengtson and J.~Parrow},
+  title     = {{P}si-{C}alculi in {I}sabelle},
+  booktitle = {Proc of the 22nd TPHOLs Conference},
+  year      = 2009,
+  pages     = {99--114},
+  series    = {LNCS},
+  volume    = {5674}
+}
+
+@inproceedings{TobinHochstadtFelleisen08,
+  author    = {S.~Tobin-Hochstadt and M.~Felleisen},
+  booktitle = {Proc.~of the 35rd POPL Symposium},
+  title     = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
+  publisher = {ACM},
+  year      = {2008},
+  pages     = {395--406}
+}
+
+@InProceedings{UrbanCheneyBerghofer08,
+  author = "C.~Urban and J.~Cheney and S.~Berghofer",
+  title = "{M}echanizing the {M}etatheory of {LF}",
+  pages = "45--56",
+  year = 2008,
+  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 RTA Conference",
+  year = "2008",
+  pages = "409--424",
+  series = "LNCS",
+  volume = 5117
 }
\ No newline at end of file