Add submissions and update bib.

bibs/header.bib

@@ -419,7 +419,7 @@
 
 % ----
 @STRING{nsdi        = "{USENIX} {S}ymposium on {N}etworked {S}ystems {D}esign
-  and {I}mplementation (NDSI)"}
+  and {I}mplementation (NSDI)"}
 @STRING{nsdi10      = nsdi # ", San Jose, California"}
 @STRING{nsdi12      = nsdi # ", San Jose, California"}
 

bibs/myrefs.bib

@@ -1,6 +1,42 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+@unpublished{BGHS16,
+  title  = {Coupling proofs are probabilistic product programs},
+  author = {Barthe, Gilles and
+            Gr{\'e}goire, Benjamin and
+            Hsu, Justin and
+            Strub, {P}ierre-{Y}ves},
+  year   = 2016,
+  jh     = yes,
+  docs   = yes
+}
+
+@unpublished{BEGGHS16,
+  title  = {Formal certification of randomized algorithms},
+  author = {Barthe, Gilles and
+            Espitau, Thomas and
+            Gaboardi, Marco and
+            Gr{\'e}goire, Benjamin and
+            Hsu, Justin and
+            Strub, {P}ierre-{Y}ves},
+  year   = 2016,
+  jh     = yes,
+  docs   = yes
+}
+
+@unpublished{ACGHK16,
+  title  = {A semantic account of metric preservation},
+  author = {de Amorim, Arthur Azevedo and
+            Cherigui, Ikram and
+            Gaboardi, Marco and
+            Hsu, Justin and
+            Katsumata, {Shin-ya}},
+  year   = 2016,
+  jh     = yes,
+  docs   = yes
+}
+
 @unpublished{BGGHS16c,
-  title  = {Advanced probabilistic couplings for differential privacy},
+  title  = {Advanced Probabilistic Couplings for Differential Privacy},
   author = {Barthe, Gilles and
             Gaboardi, Marco and
             Gr{\'e}goire, Benjamin and
@@ -41,19 +77,6 @@
   eprint = yes
 }
 
-@unpublished{BEGGHS15,
-  title  = {Formal certification of randomized algorithms},
-  author = {Barthe, Gilles and
-            Espitau, Thomas and
-            Gaboardi, Marco and
-            Gr{\'e}goire, Benjamin and
-            Hsu, Justin and
-            Strub, {P}ierre-{Y}ves},
-  year   = 2015,
-  jh     = yes,
-  docs   = yes
-}
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%% CONFERENCES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 @inproceedings{BEFFH16,
   title  = {Synthesizing probabilistic invariants via {D}oob's decomposition},

content/news.md

@@ -1,3 +1,9 @@
++ **07/2017** Our preprint **Coupling proofs are probabilistic product
+  programs** is now available.
++ **07/2016** An updated version of our preprint **Formal verification of
+  randomized algorithms** is now available.
++ **07/2016** Our preprint **A semantic account of metric preservation** is now
+  available.
 + **06/2016** Our preprint **Advanced probabilistic couplings for differential
   privacy** is now available on `arXiv`.
 + **05/2016** Our preprint **Synthesizing probabilistic invariants via Doob's