--- a/Quotient-Paper/document/root.bib	Mon Jun 21 06:46:28 2010 +0100
+++ b/Quotient-Paper/document/root.bib	Mon Jun 21 06:47:40 2010 +0100
@@ -37,7 +37,7 @@
   author    = {Laurent Chicli and
                Loic Pottier and
                Carlos Simpson},
-  title     = {Mathematical Quotients and Quotient Types in Coq},
+  title     = {{M}athematical {Q}uotients and {Q}uotient {T}ypes in {C}oq},
   booktitle = {TYPES},
   year      = {2002},
   pages     = {95-107},
@@ -128,4 +128,77 @@
         author          = "John Harrison",
         title           = "Theorem Proving with the Real Numbers",
         publisher       = "Springer-Verlag",
-        year            = 1998}
\ No newline at end of file
+        year            = 1998}
+
+@BOOK{Barendregt81,
+  AUTHOR = 	 "H.~Barendregt",
+  TITLE = 	 "{T}he {L}ambda {C}alculus: {I}ts {S}yntax and {S}emantics",
+  PUBLISHER = 	 "North-Holland",
+  YEAR = 	 1981,
+  VOLUME = 	 103,
+  SERIES = 	 "Studies in Logic and the Foundations of Mathematics"
+}
+
+@BOOK{CurryFeys58,
+  AUTHOR = 	 "H.~B.~Curry and R.~Feys",
+  TITLE = 	 "{C}ombinatory {L}ogic",
+  PUBLISHER =    "North-Holland",
+  YEAR = 	 "1958",
+  VOLUME =       1,
+  SERIES =       "Studies in Logic and the Foundations of Mathematics"
+}
+
+@Unpublished{UrbanKaliszyk11,
+  author = 	 {C.~Urban and C.~Kaliszyk},
+  title = 	 {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},
+  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