diff --git a/bibs/myrefs.bib b/bibs/myrefs.bib
index 0a6be02..de2b7d5 100644
--- a/bibs/myrefs.bib
+++ b/bibs/myrefs.bib
@@ -1,9 +1,9 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 @unpublished{SKFHKKS18,
   title    = {Probabilistic Program Equivalence for {NetKAT}},
-  author   = {Steffen Smolka and
-              Praveen Kumar and
-              Nate, Foster and
+  author   = {Smolka, Steffen and
+              Kumar, Praveen and
+              Foster, Nate and
               Hsu, Justin and
               Kahn, David and
               Kozen, Dexter and
@@ -893,14 +893,6 @@ inproceedings{HHRRW14,
   jh = yes,
 }
 
-@talk{msrc17-talk,
-  title = {From Probabilistic Coupling to Relational Program Logics},
-  organization = {Microsoft Research Cambridge},
-  year = 2017,
-  month = nov,
-  jh = yes,
-}
-
 @talk{kent17-talk,
   title = {From Probabilistic Coupling to Relational Program Logics},
   organization = {Programming Languages and Systems Seminar, University of Kent},
@@ -909,6 +901,14 @@ inproceedings{HHRRW14,
   jh = yes,
 }
 
+@talk{msrc17-talk,
+  title = {From Probabilistic Coupling to Relational Program Logics},
+  organization = {Microsoft Research Cambridge},
+  year = 2017,
+  month = nov,
+  jh = yes,
+}
+
 @talk{icalp17-talk,
   title = {$\star$-Liftings for Differential Privacy},
   organization = icalp17,
@@ -4915,7 +4915,7 @@ inproceedings{LarsenS89,
   url={https://eudml.org/doc/113445}
 }
 
-@book {RudinPMA,
+@book{RudinPMA,
   AUTHOR = {Rudin, Walter},
   TITLE = {Principles of Mathematical Analysis},
   EDITION = {Third},
@@ -6606,17 +6606,21 @@ publisher=springer
 }
 
 @article{mciver2016new,
-  title={A New Rule for Almost-Certain Termination},
-  author={McIver, Annabelle and
-          Morgan, Carroll and
-          Kaminski, Benjamin Lucien and
-          Katoen, {Joost}-{Pieter}},
-  journal  = pacmpl,
-  volume   = {1},
-  number   = {POPL},
-  note="To appear at " # popl18,
-  year={2018},
-  url={https://arxiv.org/abs/1612.01091}
+  author    = {Annabelle McIver and
+               Carroll Morgan and
+               Benjamin Lucien Kaminski and
+               Joost{-}Pieter Katoen},
+  title     = {A new proof rule for almost-sure termination},
+  journal   = pacmpl,
+  volume    = {2},
+  number    = {{POPL}},
+  pages     = {33:1--33:28},
+  year      = {2018},
+  url       = {http://doi.acm.org/10.1145/3158121},
+  doi       = {10.1145/3158121},
+  timestamp = {Fri, 05 Jan 2018 12:57:30 +0100},
+  biburl    = {http://dblp.org/rec/bib/journals/pacmpl/McIverMKK18},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
 @article{deng2009kantorovich,
@@ -6831,3 +6835,45 @@ url={https://doi.org/10.1007/3-540-48224-5_35}
   year={1967},
   publisher={Mathematical Institute, Tohoku University}
 }
+
+@book{rudin-real-complex,
+ address              = {New York},
+ author               = {Rudin, Walter},
+ edition              = {Third},
+ isbn                 = {0-07-054234-1},
+ mrclass              = {00A05 (26-01 30-01 46-01)},
+ mrnumber             = {MR924157 (88k:00002)},
+ pages                = {xiv+416},
+ publisher            = {McGraw-Hill Book Co.},
+ title                = {Real and complex analysis},
+ year                 = {1987},
+ }
+
+@article{DBLP:journals/corr/KerstanK13,
+  author    = {Henning Kerstan and
+               Barbara K{\"{o}}nig},
+  title     = {Coalgebraic Trace Semantics for Continuous Probabilistic Transition
+               Systems},
+  journal   = lmcs,
+  volume    = {9},
+  number    = {4},
+  year      = {2013},
+  url       = {https://doi.org/10.2168/LMCS-9(4:16)2013},
+  doi       = {10.2168/LMCS-9(4:16)2013},
+  timestamp = {Wed, 03 May 2017 14:47:57 +0200},
+  biburl    = {http://dblp.org/rec/bib/journals/corr/KerstanK13},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@inproceedings{Pnueli1977,
+ author = {Pnueli, Amir},
+ title = {The Temporal Logic of Programs},
+ booktitle = focs77,
+ year = {1977},
+ pages = {46--57},
+ numpages = {12},
+ url = {http://dx.doi.org/10.1109/SFCS.1977.32},
+ doi = {10.1109/SFCS.1977.32},
+ acmid = {1382534},
+}
+