diff -r d97e04126a3d -r 61d30863e5d1 Pearl-jv/document/root.bib
--- a/Pearl-jv/document/root.bib	Tue Mar 01 00:14:02 2011 +0000
+++ b/Pearl-jv/document/root.bib	Wed Mar 02 00:06:28 2011 +0000
@@ -8,6 +8,17 @@
 	year = "2008"
 }
 
+@InProceedings{norrish04,
+  author = 	 {M.~Norrish},
+  title = 	 {{R}ecursive {F}unction {D}efinition for {T}ypes with {B}inders},
+  booktitle = 	 {Proc.~of the 17th International Conference Theorem Proving in 
+                  Higher Order Logics (TPHOLs)},
+  pages = 	 {241--256},
+  year = 	 {2004},
+  volume = 	 {3223},
+  series = 	 {LNCS}
+}
+
 @InProceedings{GunterOsbornPopescu09,
   author = 	 {E.L.~Gunter and C.J.~Osborn and A.~Popescu},
   title = 	 {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in
@@ -19,6 +30,16 @@
   series = 	 {ENTCS}
 }
 
+@InProceedings{AydemirBohannonWeirich07,
+  author = 	 {B.~Aydemir and A.~Bohannon and S.~Weihrich},
+  title = 	 {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)},
+  booktitle = 	 {Proc.~of the 1st International Workshop on Logical Frameworks and Meta-Languages: 
+                  Theory and Practice (LFMTP)},
+  pages = 	 {69--77},
+  year = 	 {2007},
+  series = 	 {ENTCS}
+}
+
 @Unpublished{SatoPollack10,
   author = 	 {M.~Sato and R.~Pollack},
   title = 	 {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},