--- a/Paper/document/root.bib	Mon Feb 04 01:47:26 2013 +0000
+++ b/Paper/document/root.bib	Mon Feb 04 11:14:03 2013 +0000
@@ -1,3 +1,23 @@
+@article{Nipkow98,
+  author={T.~Nipkow},
+  title={{W}inskel is (almost) {R}ight: {T}owards a {M}echanized {S}emantics {T}extbook},
+  journal={Formal Aspects of Computing},
+  volume=10,
+  pages={171--186},
+  year=1998
+}
+
+@inproceedings{Jensen13,
+  author    = {J.~Braband Jensen and
+               N.~Benton and
+               A.~Kennedy},
+  title     = {{H}igh-{L}evel {S}eparation {L}ogic for {L}ow-{L}evel {C}ode},
+  booktitle = {Proc.~of the 40th Symposium on Principles
+               of Programming Languages (POPL)},
+  year      = {2013},
+  pages     = {301--314}
+}
+
 @article{UrbanCheneyBerghofer11,
   author = {C.~Urban and J.~Cheney and S.~Berghofer},
   title = {{M}echanizing the {M}etatheory of {LF}},