--- a/Paper/document/root.bib	Thu Mar 18 19:39:01 2010 +0100
+++ b/Paper/document/root.bib	Thu Mar 18 22:06:28 2010 +0100
@@ -9,6 +9,16 @@
   series = 	 {LNCS}
 }
 
+@INPROCEEDINGS{Pottier06,
+  author = {F.~Pottier},
+  title = {{A}n {O}verview of {C$\alpha$ml}},
+  year = {2006},
+  booktitle = {ACM Workshop on ML},
+  pages = {27--52},
+  volume = {148},
+  number = {2},
+  series = {ENTCS}
+}
 
 @Unpublished{HuffmanUrban10,
   author = 	 {B.~Huffman and C.~Urban},
@@ -32,6 +42,21 @@
   note = 	 {Personal communication.}
 }
 
+@InProceedings{challenge05,
+  author = 	 {B.~E.~Aydemir and A.~Bohannon and M.~Fairbairn and
+                  J.~N.~Foster and B.~C.~Pierce and P.~Sewell and 
+                  D.~Vytiniotis and G.~Washburn and S.~Weirich and
+                  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)},
+  pages = 	 {50--65},
+  year = 	 {2005},
+  volume = 	 {3603},
+  series = 	 {LNCS}
+}
+
 @Unpublished{SatoPollack10,
   author = 	 {M.~Sato and R.~Pollack},
   title = 	 {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},