From b907eb6fc81181db4a4d101d762eef7584698948 Mon Sep 17 00:00:00 2001 From: Justin Hsu Date: Wed, 13 May 2015 13:11:28 -0400 Subject: [PATCH] Update bib and header. --- bibs/header.bib | 24 ++- bibs/myrefs.bib | 483 ++++++++++++++++++++++++++++++++++++++++++------ 2 files changed, 441 insertions(+), 66 deletions(-) diff --git a/bibs/header.bib b/bibs/header.bib index b63f5ee..1d30836 100644 --- a/bibs/header.bib +++ b/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" } @@ -442,7 +450,7 @@ ({CoLT})}} @STRING{concur = {International Conference on Concurrency Theory (CONCUR)} } @STRING{csl = {International Workshop on Computer Science Logic (CSL)} } -@STRING{csfw = {IEEE Computer Security Foundations Workshop (CSFW) } } +@STRING{csfw = {IEEE Computer Security Foundations Workshop (CSFW)} } @STRING{ecoop = {European Conference on Object-Oriented Programming (ECOOP)} } @STRING{esop = {European Symposium on Programming (ESOP)} } @STRING{fesca = {International Workshop on Formal Engineering approaches to @@ -470,10 +478,10 @@ Practice of Declarative Programming (PPDP)} } @STRING{randapx = {Workshop on Approximation Algorithms for Combinatorial Optimization Problems (APPROX) and Workshop on Randomization - and Computation (RANDOM) } } + and Computation (RANDOM)} } @STRING{rta = {International Conference on Rewriting Techniques and Applications (RTA)} } -@STRING{sas = {International Symposium on Static Analysis (SAS) } } +@STRING{sas = {International Symposium on Static Analysis (SAS)} } @STRING{sosp = {ACM Symposium on Operating Systems Principles (SOSP)} } @STRING{tacs = {International Symposium on Theoretical Aspects of Computer Software (TACS)} } @@ -486,14 +494,14 @@ @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)} } @STRING{wosn = {Workshop on Online Social Networks (WOSN)} } @STRING{xsym = {Database and XML Technologies: International XML Database Symposium (XSym)} } -@STRING{wsa = {Workshop on Static Analysis (WSA) } } +@STRING{wsa = {Workshop on Static Analysis (WSA)} } % ---- % Specific meetings, with locations: % --- @@ -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" } diff --git a/bibs/myrefs.bib b/bibs/myrefs.bib index 7b71060..a68ceb8 100644 --- a/bibs/myrefs.bib +++ b/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, - 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, +@inproceedings{HGH14, 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}, +}