diff -r 1801cc460fc9 -r 2eafd8ed4bbf Paper/document/root.bib
--- a/Paper/document/root.bib	Tue Mar 30 22:31:15 2010 +0200
+++ b/Paper/document/root.bib	Wed Mar 31 02:59:18 2010 +0200
@@ -1,3 +1,27 @@
+@InProceedings{LeeCraryHarper07,
+  author = 	 {D.~K.~Lee and K.~Crary and R.~Harper},
+  title = 	 {{T}owards a {M}echanized {M}etatheory of {Standard ML}},
+  booktitle =    {Proc.~of the 34th POPL Symposium},
+  year = 	 2007,
+  pages =        {173--184}
+}
+
+@Unpublished{chargueraud09,
+  author       = "Arthur Chargu{\'e}raud",
+  title        = "{T}he {L}ocally {N}ameless {R}epresentation",
+  year         = "2009",
+  note         = "To appear in J.~of Automated Reasoning. 
+                  {http://arthur.chargueraud.org/research/2009/ln/}",
+}
+
+@article{NaraschewskiNipkow99,
+  author={W.~Naraschewski and T.~Nipkow},
+  title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}},
+  journal={J.~of Automated Reasoning},
+  year=1999,
+  volume=23,
+  pages={299--318}}
+
 @InProceedings{Berghofer99,
   author = 	 {S.~Berghofer and M.~Wenzel},
   title = 	 {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in 
@@ -142,8 +166,8 @@
 
 @article{Pitts03,
   author =	 {A.~M.~Pitts},
-  title =	 {Nominal Logic, A First Order Theory of Names and
-                  Binding},
+  title =	 {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and
+                  {B}inding},
   journal =	 {Information and Computation},
   year =	 {2003},
   volume =	 {183},