Update bib and header.

bibs/header.bib

@@ -62,6 +62,7 @@
 % %%%%%%%%%%%%%%%%%%%%%%
 @STRING{toplas   = "ACM Transactions on Programming Languages and Systems" }
 @STRING{jlp      = {Journal of Logic Programming} }
+@STRING{ieee = "IEEE" }
 @STRING{acmpress = "ACM Press" }
 @STRING{cacm     = "Communications of the {ACM}" }
 @STRING{jacm     = "Journal of the {ACM}" }
@@ -166,6 +167,7 @@
                       {F}unctional {P}rogramming ({ICFP})" }
 @STRING{icfp14      = icfp # ", Gothenburg, Sweden" }
 @STRING{icfp13      = icfp # ", Boston, Massachusetts" }
+@STRING{icfp12      = icfp # ", Copenhagen, Denmark" }
 @STRING{icfp11      = icfp # ", Tokyo, Japan" }
 @STRING{icfp10      = icfp # ", Baltimore, Maryland" }
 @STRING{icfp08      = icfp # ", Victoria, British Colombia" }
@@ -180,6 +182,9 @@
 @STRING{icfp97      = icfp # ", Amsterdam, The Netherlands" }
 @STRING{icfp96      = icfp # ", Philadelphia, Pennsylvania" }
 % ----
+@STRING{itp         = "Interactive Theorem Proving"}
+@STRING{itp13       = itp # ", Rennes, France" }
+% ----
 @STRING{oopsla      = "{ACM} {SIGPLAN} {C}onference on {O}bject {O}riented
                       {P}rogramming: {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})" }
 @STRING{oopslapre96 = "{C}onference on {O}bject {O}riented {P}rogramming:
@@ -223,6 +228,7 @@
 @STRING{lics01      = lics # ", Boston, Massachusetts" }
 @STRING{lics02      = lics # ", Copenhagen, Denmark" }
 @STRING{lics03      = lics # ", Ottawa, Ontario" }
+@STRING{lics06      = lics # ", Seattle, Washington" }
 @STRING{lics11      = lics # ", Toronto, Ontario" }
 % ----
 @STRING{pldi        = "{ACM SIGPLAN Conference on Programming Language Design
@@ -376,6 +382,7 @@
 % ----
 @STRING{sigmod      = "{ACM} {SIGMOD} {I}nternational {C}onference on
   {M}anagement of {D}ata (SIGMOD)"}
+@STRING{sigmod00    = sigmod # ", New York, New York"}
 @STRING{sigmod09    = sigmod # ", Providence, Rhode Island"}
 @STRING{sigmod10    = sigmod # ", Indianapolis, Indiana"}
 @STRING{sigmod14    = sigmod # ", Snowbird, Utah"}
@@ -407,6 +414,7 @@
 @STRING{csf      = "{IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium
                    ({CSF})" }
 @STRING{csf08    = csf # ", Pittsburgh, Pennsylvania" }
+@STRING{csf11    = csf # ", Domaine de l'Abbaye des Vaux de Cernay, France" }
 @STRING{csf13    = csf # ", New Orleans, Louisiana" }
 @STRING{csf14    = csf # ", Vienna, Austria" }
 
@@ -486,7 +494,7 @@
 @STRING{tldi      = {ACM SIGPLAN Workshop on Types in Language Design and
                     Implementation (TLDI)} }
 @STRING{tphol     = {International Conference on Theorem Proving in Higher Order
-                    Logics } }
+                    Logics (TPHOL)} }
 @STRING{types     = {International Workshop on Types for Proofs and Programs
                     (TYPES)} }
 @STRING{webdb     = {International Workshop on the Web and Databases (WebDB)} }
@@ -517,6 +525,7 @@
 @STRING{cav96       = cav # ", New Brunswick, New Jersey" }
 @STRING{cav02       = cav # ", Copenhagen, Denmark" }
 @STRING{cav07       = cav # ", Berlin, Germany" }
+@STRING{cav13       = cav # ", Saint Petersburg, Russia" }
 % ---
 @STRING{cp          = "International Conference on Principles and Practice of
                        Constraint Programming (CP)" }
@@ -547,6 +556,7 @@
 @STRING{esop02      = esop # ", Grenoble, France" }
 @STRING{esop09      = esop # ", York, England" }
 @STRING{esop11      = esop # ", Saarbr{\"u}cken, Germany" }
+@STRING{esop13      = esop # ", Rome, Italy" }
 @STRING{esop14      = esop # ", Grenoble, France" }
 % ---
 @STRING{fesca14     = fesca # ", Grenoble, France" }
@@ -562,6 +572,7 @@
 % ---
 @STRING{icalp98     = icalp # ", Aalborg, Denmark" }
 @STRING{icalp06     = icalp # ", Venice, Italy" }
+@STRING{icalp11     = icalp # ", Z{\"u}rich, Switzerland" }
 @STRING{icalp12     = icalp # ", Warwick, England" }
 @STRING{icalp13     = icalp # ", Riga, Latvia" }
 @STRING{icalp14     = icalp # ", Copenhagen, Denmark" }
@@ -615,13 +626,14 @@
 @STRING{tlca03      = tlca # ", Valencia, Spain" }
 % ---
 @STRING{tldi03      = tldi # ", New Orleans, Louisiana"}
+@STRING{tldi12      = tldi # ", Philadelphia, Pennsylvania"}
 % ---
 @STRING{tphol09     = tphol # ", Munich, Germany" }
 % ---
 @STRING{types93     = types # ", Nijmegen, The Netherlands" }
 @STRING{types98     = types # ", Kloster Irsee, Germany" }
 % ---
-@STRING{uai         = "Conference on Uncertainty in Artificial Intelligence (UAI)"}
+@STRING{uai         = "Conference on Uncertainty in Artificial Intelligence ({UAI})"}
 @STRING{uai02       = uai # ", Edmonton, Alberta" }
 % ---
 @STRING{wosn12      = wosn # ", Helsinki, Finland" }

bibs/myrefs.bib

@@ -385,14 +385,6 @@
   year      = 2007
 }
 
-@inproceedings{l-diversity,
-  author    = {Machanavajjhala, A. and Gehrke, J. and Kifer, D. and Venkitasubramaniam, M.},
-  title     = {$l$-{D}iversity: {P}rivacy beyond $k$-anonymity},
-  booktitle = icde06,
-  url       = {http://dl.acm.org/citation.cfm?id=1217302},
-  year      = 2006
-}
-
 @article{k-anonymity,
  author  = {Sweeney, Latanya},
  title   = {$k$-{A}nonymity: {A} model for protecting privacy},
@@ -457,18 +449,7 @@
   year    = {2011}
 }
 
-@inproceedings{k-anon-attack,
+@inproceedings{HGH14,
-  author    = {Srivatsava Ranjit Ganta and
-               Shiva Prasad Kasiviswanathan and
-               Adam Smith},
-  title     = {Composition attacks and auxiliary information in data privacy},
-  booktitle = kdd08,
-  pages     = {265--273},
-  year      = 2008,
-  url       = {http://arxiv.org/abs/0803.0032}
-}
-
-@inproceedings{HGH+13,
   author    = {Hsu, Justin and
                Gaboardi, Marco and
                Haeberlen, Andreas and
@@ -497,7 +478,7 @@
   url       = {http://dl.acm.org/citation.cfm?id=2103670}
 }
 
-@inproceedings{fuzz,
+@inproceedings{ReedPierce10,
   author    = {Jason Reed and Benjamin C Pierce},
   title     = {Distance Makes the Types Grow Stronger: {A} Calculus for
     Differential Privacy},
@@ -866,6 +847,7 @@
   title     = {Tridirectional typechecking},
   booktitle = popl04,
   pages     = {281--292},
+  year      = 2004,
   url       =
   {http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking/Dunfield04_tridirectional.pdf}
 }
@@ -1262,18 +1244,19 @@ url          = {http://research.microsoft.com/pubs/208236/asplos077-bornholtA.pd
 }
 
 
-@techreport{BUCS-TR-2008--026,
+@techreport{BUCS-TR-2008-026,
 author = {Andrei Lapets and Alex Levin and David Parkes},
 title = {{A Typed Truthful Language for One-dimensional Truthful Mechanism Design}},
 number = {BUCS-TR-2008--026},
 year = {2008},
+institution = {Boston University},
 url = {http://cs-people.bu.edu/lapets/resource/typed-ec-mech.pdf}
 }
 
 @misc{Fang14,
 author = {Ye Fang and Swarat Chaudhuri and  Moshe Vardi},
 title = {{Computer-aided mechanism design}},
-note = {Poster at POPL'14},
+howpublished = {Poster at POPL'14},
 year = {2014}
 }
 
@@ -1332,7 +1315,7 @@ year = {2014}
 
 @inproceedings{ZaksP08,
   author    = {Anna Zaks and Amir Pnueli},
-  title     = {CoVaC: Compiler Validation by Program Analysis of the Cross-Product},
+  title     = {{CoVaC}: Compiler Validation by Program Analysis of the Cross-Product},
   booktitle = fm08,
   pages     = {35--51},
   publisher = {Springer},
@@ -1429,8 +1412,6 @@ year = {2014}
   title={Verifying higher-order functional programs with pattern-matching algebraic data types},
   author={Ong, C-H Luke and Ramsay, Steven James},
   booktitle=popl11,
-  volume={46},
-  number={1},
   pages={587--598},
   year={2011},
   url={https://www.cs.ox.ac.uk/files/3721/main.pdf}
@@ -1440,7 +1421,7 @@ year = {2014}
   author    = {Benjamin C Pierce},
   title     = {Differential Privacy in the Programming Languages Community},
   year      = {2012},
-  note      = {Invited tutorial at DIMACS Workshop on Recent Work on
+  howpublished      = {Invited tutorial at DIMACS Workshop on Recent Work on
                Differential Privacy across Computer Science}
 }
 
@@ -1774,6 +1755,7 @@ year = {2014}
   year      = {2015},
   url       = {http://arxiv.org/abs/1407.6845},
   jh        = yes,
+  slides    = yes,
   eprint    = yes
 }
 
@@ -2108,8 +2090,8 @@ year = {2014}
   title     = {A Theory {AB} Toolbox},
   year      = {2015},
   booktitle = snapl15,
-  note      = {To appear.},
   jh        = yes,
+  slides    = yes,
   docs      = yes
 } 
 
@@ -2117,9 +2099,9 @@ year = {2014}
   author    = {Justin Hsu},
   title     = {Death, Taxes, and Formal Verification (Abstract)},
   year      = {2015},
-  note      = {To appear.},
   booktitle = snapl15,
   jh        = yes,
+  slides    = yes,
   docs      = yes
 } 
 
@@ -2287,17 +2269,9 @@ verification conditions},
   author={Roughgarden, Tim},
   volume={174},
   year={2005},
-  publisher={MIT press Cambridge}
+  publisher=mitpress
 }
 
-@article{Chadha:2007,
-	Author = {Chadha, R. and Cruz-Filipe, L. and Mateus, P. and Sernadas, A.},
-	Journal = tcs,
-	Number = {1-2},
-	Title = {Reasoning about probabilistic sequential programs},
-	Volume = {379},
-	Year = {2007}}
-
 @article{Morgan:1996,
   author    = {C Morgan and
                A Mc{I}ver and
@@ -2318,14 +2292,6 @@ verification conditions},
   year      = {1985}
 }
 
-@article{Chadha:2007,
-	Author = {Chadha, R. and Cruz-Filipe, L. and Mateus, P. and Sernadas, A.},
-	Journal = tcs,
-	Number = {1-2},
-	Title = {Reasoning about probabilistic sequential programs},
-	Volume = {379},
-	Year = {2007}}
-
 @article{Morgan:1996,
   author    = {C Morgan and
                A Mc{I}ver and
@@ -2441,7 +2407,7 @@ language={English}
   journal-url =  "http://portal.acm.org/browse_dl.cfm?idx=J401",
 }
 
-@inproceedings{DBLP:conf/itp/GonthierAABCGRMOBPRSTT13,
+@inproceedings{Gonthier13,
   author    = {Georges Gonthier and
                Andrea Asperti and
                Jeremy Avigad and
@@ -2450,7 +2416,7 @@ language={English}
                Fran{\c{c}}ois Garillot and
                St{\'{e}}phane Le Roux and
                Assia Mahboubi and
-               Russell O'Connor and
+               Russell O'{C}onnor and
                Sidi Ould Biha and
                Ioana Pasca and
                Laurence Rideau and
@@ -2464,17 +2430,6 @@ language={English}
   doi       = {10.1007/978-3-642-39634-2_14},
 }
 
-@article{vickrey61,
-  title={Counterspeculation, auctions, and competitive sealed tenders},
-  author={Vickrey, William},
-  journal={The Journal of finance},
-  volume={16},
-  number={1},
-  pages={8--37},
-  year={1961},
-  publisher={Wiley Online Library}
-}
-
 @article{clarke71,
   title={Multipart pricing of public goods},
   author={Clarke, Edward H},
@@ -2561,7 +2516,7 @@ language={English}
   docs      = yes
 }
 
-@unpublished{HKM-verif,
+@unpublished{HKM-verif15,
   title     = {Computer-aided verification in mechanism design},
   author    = {Barthe, Gilles and
                Gaboardi, Marco and
@@ -2574,3 +2529,411 @@ language={English}
   jh        = yes,
   eprint    = yes
 }
+
+@inproceedings{HPN11,
+  title={Differential Privacy Under Fire},
+  author={Haeberlen, Andreas and
+          Pierce, Benjamin C and
+          Narayan, Arjun},
+  booktitle={USENIX Security Symposium},
+  year={2011}
+}
+
+@article{Girard87,
+  title={{Linear logic}},
+  author={Girard, J.Y.},
+  journal=tcs,
+  volume={50},
+  number={1},
+  pages={1--102},
+  year={1987},
+  publisher={Elsevier}
+}
+
+@incollection{Walker-atapl,
+  author = 	 {David Walker},
+  title = 	 {Substructural Type Systems},
+  booktitle = 	 {Advanced Topics in Types and Programming Languages},
+  editor = {Benjamin C Pierce},
+  publisher = 	 mitpress,
+  year = 	 {2005},
+}
+
+@article{BLL,
+  title={{Bounded linear logic}},
+  author={Girard, J.Y. and Scedrov, A. and Scott, P.},
+  journal=tcs,
+  volume={97},
+  number={1},
+  pages={1--66},
+  year={1992}
+}
+
+@inproceedings{WrightBaker93,
+  title={{Usage Analysis with Natural Reduction Types}},
+  author={Wright, D.A. and Baker-Finch, C.A.},
+  booktitle={International Workshop on Static Analysis},
+  pages={254--266},
+  year={1993},
+  publisher=springer
+}
+
+@InProceedings{DalLagoHofmann09,
+  title =	"Bounded Linear Logic, Revisited",
+  author =	"Dal Lago, Ugo and Hofmann, Martin",
+  booktitle =	tlca,
+  publisher =	springer,
+  year = 	"2009",
+  volume =	"5608",
+  pages =	"80--94",
+  series =	lncs,
+}
+
+@InProceedings{XiPfenning99,
+  author =	"Hongwei Xi and Frank Pfenning",
+  title =	"Dependent Types in Practical Programming",
+  pages =	"214--227",
+  booktitle =	popl99,
+  year = 	"1999",
+}
+
+@InProceedings{ATS,
+  title =	"Combining programming with theorem proving",
+  author =	"Chiyan Chen and Hongwei Xi",
+  booktitle =	icfp05,
+  year = 	"2005",
+  pages =	"66--77",
+  url =  	"http://doi.acm.org/10.1145/1086365.1086375",
+}
+
+@article{McBrideMcKinna02,
+  author = 	 {Conor Mc{B}ride and James Mc{K}inna},
+  title = 	 {The view from the left},
+  journal =      jfp,
+  year = {2004}, 
+  pages = "69--111",
+  volume = 14,
+  number = 1,
+}
+
+@inproceedings{weirich-promotion,
+  author = {Yorgey, Brent A and
+            Weirich, Stephanie and 
+            Cretin, Julien and
+            {Peyton Jones}, Simon and 
+            Vytiniotis, Dimitrios and
+            Magalha\~{e}s, Jos\'{e} Pedro},
+  title = {Giving Haskell A Promotion},
+  booktitle = tldi12,
+  year = 2012,
+  url = {http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf},
+}
+
+@Article{cervesato-llf,
+  title =	"A Linear Logical Framework",
+  author =	"Iliano Cervesato and Frank Pfenning",
+  journal =	ic,
+  month =	nov,
+  year = 	"2002",
+  volume =	"179",
+  number =	"1",
+  pages =	"19--75",
+}
+
+@InProceedings{watkins03types,
+  author =	"Keven Watkins and Iliano Cervesato and Frank Pfenning
+		 and David Walker",
+  title =	"A concurrent logical framework {I}: The propositional
+		 fragment",
+  booktitle =	types,
+  volume = 3085,
+  series = lncs, 
+  publisher = springer,
+  year = 	"2003",
+}
+
+@InProceedings{DLG11,
+author= {Dal Lago, Ugo and
+         Gaboardi, Marco},
+title="Linear Dependent Types and Relative Completeness",
+  booktitle = lics11,
+ pages = "133--142",
+year={2011}
+}
+
+@InProceedings{KTDG12,
+  title =	"Superficially Substructural Types",
+  author =	"Krishnaswami, Neelakantan R. and Turon, Aaron and Dreyer, Derek and Garg, Deepak",
+  booktitle =	icfp12,
+  year = 	2012,
+}
+
+@misc{PalamidessiStronati12,
+  title={Differential privacy for relational algebra: Improving the
+    sensitivity bounds via constraint systems},
+  author={Palamidessi, Catuscia and Stronati, Marco},
+  note={arXiv preprint arXiv:1207.0872},
+  year={2012}
+}
+
+@inproceedings{CGL10,
+ author = {Chaudhuri, Swarat and Gulwani, Sumit and Lublinerman, Roberto},
+ title = {Continuity analysis of programs},
+ booktitle = popl10,
+ year = {2010},
+ pages = {57--70},
+ doi = {http://doi.acm.org/10.1145/1707801.1706308},
+}
+
+@InProceedings{CGLN11,
+  title =	"Proving programs robust",
+  author =	"Swarat Chaudhuri and Sumit Gulwani and Roberto
+		 Lublinerman and Sara NavidPour",
+  booktitle =	{ {ACM} {SIGSOFT} Symposium on the Foundations of Software
+    Engineering ({FSE}), Szeged, Hungary },
+  year = 	"2011",
+  ISBN = 	"978-1-4503-0443-6",
+  pages =	"102--112",
+  URL =  	"http://doi.acm.org/10.1145/2025113.2025131",
+}
+
+@INPROCEEDINGS{Lowe-QIF02,
+    author = {Gavin Lowe},
+    title = {Quantifying Information Flow},
+    booktitle = csfw02,
+    year = {2002},
+    pages = {18--31}
+}
+
+@inproceedings{McCamantErnst08,
+ author = {McCamant, Stephen and Ernst, Michael D.},
+ title = {Quantitative information flow as network flow capacity},
+ booktitle = pldi08,
+ year = {2008},
+ isbn = {978-1-59593-860-2},
+ pages = {193--205},
+ doi = {http://doi.acm.org/10.1145/1375581.1375606},
+ address = {New York, NY, USA},
+ }
+
+@inproceedings{AACP11,
+  author = {Alvim, S., M{\'a}rio and Andres, E., Miguel and Chatzikokolakis, Konstantinos and Palamidessi, Catuscia},
+  title = {{On the relation between Differential Privacy and Quantitative Information Flow}},
+  booktitle = icalp11,
+  year = {2011},
+  series = lncs,
+  doi = {10.1007/978-3-642-22012-8_4},
+  publisher = springer,
+  volume = {6756},
+  pages = {60--76},
+  url = {http://hal.inria.fr/inria-00627937/en},
+}
+
+@inproceedings{barthekoepf11,
+ author = {Gilles Barthe and Boris K{\"o}pf},
+ title  = {{Information-theoretic Bounds for Differentially Private Mechanisms}},
+ booktitle = csf11,
+ publisher = ieee,
+ pages = {191--204},
+ year = {2011}
+}
+
+@inproceedings{AgrawalSrikant00,
+  title={Privacy-preserving data mining},
+  author={Agrawal, Rakesh and Srikant, Ramakrishnan},
+  booktitle=sigmod00,
+  pages={439--450},
+  year={2000},
+}
+
+@article{l-diversity,
+  title={l-diversity: Privacy beyond k-anonymity},
+  author={Machanavajjhala, Ashwin and Kifer, Daniel and Gehrke, Johannes and
+    Venkitasubramaniam, Muthuramakrishnan},
+  journal={{ACM} Transactions on Knowledge Discovery from Data ({TKDD})},
+  volume={1},
+  number={1},
+  pages={3},
+  year={2007},
+  publisher={ACM}
+}
+
+@article{ESA04,
+  title={Privacy preserving mining of association rules},
+  author={Evfimievski, Alexandre and Srikant, Ramakrishnan and Agrawal,
+    Rakesh and Gehrke, Johannes},
+  journal={Information Systems},
+  volume={29},
+  number={4},
+  pages={343--364},
+  year={2004},
+  publisher=elsevier
+}
+
+@inproceedings{GKSS08,
+  title={Composition attacks and auxiliary information in data privacy},
+  author={Ganta, Srivatsava Ranjit and Kasiviswanathan, Shiva Prasad and
+    Smith, Adam},
+  booktitle=kdd08,
+  pages={265--273},
+  year={2008},
+}
+
+@book{Hurwicz60,
+  title={Optimality and informational efficiency in resource allocation
+    processes},
+  author={Hurwicz, Leonid},
+  year={1960},
+  publisher={Stanford University Press}
+}
+
+@article{Vickrey61,
+  title={Counterspeculation, auctions, and competitive sealed tenders},
+  author={Vickrey, William},
+  journal={The Journal of Finance},
+  volume={16},
+  number={1},
+  pages={8--37},
+  year={1961},
+}
+
+@article{Hurwicz72,
+  title={On informationally decentralized systems},
+  author={Hurwicz, Leonid},
+  journal={Decision and organization},
+  year={1972},
+  publisher={North-Holland Amsterdam}
+}
+
+@article{Myerson08,
+  title={Perspectives on mechanism design in economic theory},
+  author={Myerson, Roger B},
+  journal={The American Economic Review},
+  pages={586--603},
+  year={2008},
+  publisher={JSTOR}
+}
+
+@incollection{BGBP-bigops08,
+  title={Canonical big operators},
+  author={Bertot, Yves and Gonthier, Georges and Biha, Sidi Ould and Pasca,
+    Ioana},
+  booktitle=tphol,
+  pages={86--101},
+  year={2008},
+  publisher=springer
+}
+
+@techreport{Ramshaw79,
+  title={Formalizing the Analysis of Algorithms.},
+  author={Ramshaw, Lyle Harold},
+  year={1979},
+  institution={Stanford University},
+  note={STAN-CS-79-741}
+}
+
+@article{HartogVink02,
+  title={Verifying probabilistic programs using a Hoare like logic},
+  author={den Hartog, J I and de Vink, Erik P},
+  journal={International Journal of Foundations of Computer Science},
+  volume={13},
+  number={03},
+  pages={315--340},
+  year={2002},
+  publisher={World Scientific}
+}
+
+@article{Chadha07,
+  title={Reasoning about probabilistic sequential programs},
+  author={Chadha, Rohit and Cruz-Filipe, Lu{\'\i}s and Mateus, Paulo and
+    Sernadas, Am{\'\i}lcar},
+  journal=tcs,
+  volume={379},
+  number={1},
+  pages={142--165},
+  year={2007},
+  publisher=elsevier
+}
+
+@misc{RandZdancewic15,
+  author = {Rand, Robert and Zdancewic, Steve},
+  title = {A Formally Verified Probabilistic Hoare Logic with Non-Termination},
+  year = 2015
+}
+
+@article{Kozen81,
+  title={Semantics of probabilistic programs},
+  author={Kozen, Dexter},
+  journal={Journal of Computer and System Sciences},
+  volume={22},
+  number={3},
+  pages={328--350},
+  year={1981},
+  publisher={Elsevier}
+}
+
+@article{HSP83,
+  title={Termination of probabilistic concurrent program},
+  author={Hart, Sergiu and Sharir, Micha and Pnueli, Amir},
+  journal=toplas,
+  volume={5},
+  number={3},
+  pages={356--380},
+  year={1983},
+}
+
+@inproceedings{Hurd02,
+  title={A formal approach to probabilistic termination},
+  author={Hurd, Joe},
+  booktitle=tphol,
+  pages={230--245},
+  year={2002},
+  publisher=springer
+}
+
+@inproceedings{Chakarov-martingale,
+  title={Probabilistic program analysis with martingales},
+  author={Chakarov, Aleksandar and Sankaranarayanan, Sriram},
+  booktitle=cav13,
+  pages={511--526},
+  year={2013},
+  organization=springer
+}
+
+@inproceedings{FerrerHermanns15,
+  title={Probabilistic Termination: Soundness, Completeness, and
+    Compositionality},
+  author={Ferrer Fioriti, Luis Mar{\'\i}a and Hermanns, Holger},
+  booktitle=popl15,
+  pages={489--501},
+  year={2015},
+  organization={ACM}
+}
+
+@inproceedings{Kozen06,
+  title={Coinductive Proof Principles for Stochastic Processes},
+  author={Kozen, Dexter},
+  booktitle=lics06,
+  pages={359--366},
+  year={2006},
+  organization=ieee
+}
+
+@inproceedings{liquid-haskell,
+  title={Abstract refinement types},
+  author={Vazou, Niki and Rondon, Patrick M and Jhala, Ranjit},
+  booktitle=esop13,
+  pages={209--228},
+  year={2013},
+  publisher=springer
+}
+
+@inproceedings{liquid-ml,
+  title={Liquid types},
+  author={Rondon, Patrick M and Kawaguci, Ming and Jhala, Ranjit},
+  booktitle=pldi08,
+  volume={43},
+  number={6},
+  pages={159--169},
+  year={2008},
+}