diff --git a/bibs/myrefs.bib b/bibs/myrefs.bib
index 234512e..eba7889 100644
--- a/bibs/myrefs.bib
+++ b/bibs/myrefs.bib
@@ -471,7 +471,7 @@
   url       = {http://arxiv.org/abs/0803.0032}
 }
 
-@inproceedings{HGH+14,
+@inproceedings{HGH+13,
   author    = {Justin Hsu and
                Marco Gaboardi and
                Andreas Haeberlen and
@@ -1518,6 +1518,7 @@ year = {2014}
   year      = {2014},
   url       = {http://arxiv.org/abs/1402.1526},
   jh        = yes,
+  slides    = yes,
   poster    = yes,
   eprint    = yes
 }
@@ -2030,3 +2031,104 @@ year = {2014}
   jh        = yes,
   eprint    = yes
 } 
+
+@article{LovaszLocal,
+  title={Problems and results on 3-chromatic hypergraphs and some related
+    questions},
+  author={Erdos, Paul and Lov{\'a}sz, L{\'a}szl{\'o}},
+  journal={Infinite and finite sets},
+  volume={10},
+  pages={609--627},
+  year={1975}
+}
+
+@article{erdosPM,
+  title={Graph theory and probability},
+  author={Paul Erd{\H{o}}s},
+  journal={Canadian Journal of Mathematics},
+  volume={11},
+  pages={34--38},
+  year={1959}
+}
+
+@inproceedings{DBLP:conf/pldi/SampsonPMMGC14,
+  author    = {Adrian Sampson and
+               Pavel Panchekha and
+               Todd Mytkowicz and
+               Kathryn S McKinley and
+               Dan Grossman and
+               Luis Ceze},
+  title     = {Expressing and verifying probabilistic assertions},
+  booktitle = pldi14,
+  pages     = {112--122},
+  year      = {2014},
+  url       = {http://doi.acm.org/10.1145/2594291.2594294},
+  doi       = {10.1145/2594291.2594294},
+} 
+@inproceedings{DBLP:conf/pldi/CarbinKMR12,
+  author    = {Michael Carbin and
+               Deokhwan Kim and
+               Sasa Misailovic and
+               Martin C Rinard},
+  title     = {Proving acceptability properties of relaxed nondeterministic approximate
+               programs},
+  booktitle = pldi12,
+  pages     = {169--180},
+  year      = {2012},
+  url       = {http://doi.acm.org/10.1145/2254064.2254086},
+}
+
+@article{alea,
+  title     = {Proofs of randomized algorithms in Coq},
+  author    = {Audebaud, Philippe and Paulin-Mohring, Christine},
+  journal   = {Science of Computer Programming},
+  volume    = {74},
+  number    = {8},
+  pages     = {568--589},
+  year      = {2009},
+  publisher = elsevier
+}
+
+@inproceedings{DBLP:conf/pldi/SampsonPMMGC14,
+  author    = {Adrian Sampson and
+               Pavel Panchekha and
+               Todd Mytkowicz and
+               Kathryn S McKinley and
+               Dan Grossman and
+               Luis Ceze},
+  title     = {Expressing and verifying probabilistic assertions},
+  booktitle = pldi14,
+  pages     = {14},
+  year      = {2014},
+  url       = {http://doi.acm.org/10.1145/2594291.2594294},
+  doi       = {10.1145/2594291.2594294},
+} 
+@inproceedings{DBLP:conf/pldi/CarbinKMR12,
+  author    = {Michael Carbin and
+               Deokhwan Kim and
+               Sasa Misailovic and
+               Martin C Rinard},
+  title     = {Proving acceptability properties of relaxed nondeterministic approximate
+               programs},
+  booktitle = pldi12,
+  pages     = {169--180},
+  year      = {2012},
+  url       = {http://doi.acm.org/10.1145/2254064.2254086},
+}
+
+@unpublished{GHaccuracy,
+  author    = {Marco Gaboardi and
+               Justin Hsu},
+  title     = {A Theory {AB} Toolbox},
+  year      = {2015},
+  jh        = yes,
+  docs      = yes
+} 
+
+@unpublished{HsuTaxes,
+  author    = {Justin Hsu},
+  title     = {Death, Taxes, and Formal Verification},
+  year      = {2015},
+  jh        = yes,
+  docs      = yes
+} 
diff --git a/content/news.md b/content/news.md
index 25d6e94..5f1c9cb 100644
--- a/content/news.md
+++ b/content/news.md
@@ -1,4 +1,6 @@
++ **01/2015** Our abstract **Death, Taxes, and Formal Verification** has been uploaded.
++ **01/2015** Our paper **A Theory AB Toolbox** has been uploaded.
 + **11/2014** Our paper **Jointly private convex programming** has been uploaded to
   `arxiv`.
-+ **9/2014** Our paper **Higher-order refinement types for mechanism design and
++ **09/2014** Our paper **Higher-order refinement types for mechanism design and
   differential privacy** has been accepted to POPL 2015!
diff --git a/files/docs/GHaccuracypaper.pdf b/files/docs/GHaccuracypaper.pdf
new file mode 100644
index 0000000..6e9ab61
Binary files /dev/null and b/files/docs/GHaccuracypaper.pdf differ
diff --git a/files/docs/HsuTaxespaper.pdf b/files/docs/HsuTaxespaper.pdf
new file mode 100644
index 0000000..438e140
Binary files /dev/null and b/files/docs/HsuTaxespaper.pdf differ