From 87cbe4ad7d68a560c2d2acf0f2d528764bd0dc6b Mon Sep 17 00:00:00 2001 From: Justin Hsu Date: Tue, 27 Mar 2018 22:36:09 -0400 Subject: [PATCH] Add equivalence for probabilistic NetKAT draft. --- bibs/header.bib | 8 ++- bibs/myrefs.bib | 149 +++++++++++++++++++++++++++++++++++++++++++----- content/news.md | 5 +- 3 files changed, 144 insertions(+), 18 deletions(-) diff --git a/bibs/header.bib b/bibs/header.bib index 8ed75b3..732fe31 100644 --- a/bibs/header.bib +++ b/bibs/header.bib @@ -200,6 +200,7 @@ @STRING{icfp96 = icfp # ", Philadelphia, Pennsylvania" } % ---- @STRING{itp = "Interactive Theorem Proving ({ITP})"} +@STRING{itp10 = itp # ", Edinburgh, Scotland" } @STRING{itp11 = itp # ", Nijmegen, The Netherlands" } @STRING{itp13 = itp # ", Rennes, France" } % ---- @@ -231,6 +232,7 @@ @STRING{oopsla90 = oopslapre96 # "/" # ecoop # ", Ottawa, Ontario" } @STRING{oopsla98 = oopsla # ", Vancouver, British Columbia" } @STRING{oopsla03 = oopsla # ", Anaheim, California" } +@STRING{oopsla13 = oopsla # ", Indianapolis, Indiana" } @STRING{oopsla14 = oopsla # ", Portland, Oregon" } % ---- @STRING{lics = "{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS})" } @@ -321,6 +323,8 @@ % ---- @STRING{stoc = "{ACM} {SIGACT} {S}ymposium on {T}heory of {C}omputing (STOC)"} +@STRING{stoc80 = stoc # ", Los Angeles, California"} +@STRING{stoc81 = stoc # ", Milwaukee, Wisconsin"} @STRING{stoc82 = stoc # ", San Francisco, California"} @STRING{stoc83 = stoc # ", Boston, Massachusetts"} @STRING{stoc87 = stoc # ", New York, New York"} @@ -608,8 +612,8 @@ Application of Cryptology and Information Security (ASIACRYPT)" } @STRING{ascrypt15 = ascrypt # ", Auckland, New Zealand" } %---- -@STRING{asplos14 = aplas # ", Salt Lake City, Utah" } -@STRING{asplos06 = aplas # ", San Jose, California" } +@STRING{asplos14 = asplos # ", Salt Lake City, Utah" } +@STRING{asplos06 = asplos # ", San Jose, California" } %---- @STRING{ceemas07 = ceemas # ", Leipzig, Germany" } % --- diff --git a/bibs/myrefs.bib b/bibs/myrefs.bib index 3bd7b3b..54c2349 100644 --- a/bibs/myrefs.bib +++ b/bibs/myrefs.bib @@ -1,4 +1,21 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +@unpublished{SKFHKKS18, + title = {Probabilistic Program Equivalence for {NetKAT}}, + author = {Steffen Smolka and + Praveen Kumar and + Nate, Foster and + Hsu, Justin and + Kahn, David and + Kozen, Dexter and + Silva, Alexandra}, + year = {2018}, + jh = yes, + url = {https://arxiv.org/abs/1707.02772}, + eprint = {1707.02772}, + archivePrefix = {arXiv}, + primaryClass = {cs.PL}, +} + @unpublished{ABHS18, title = {Almost Sure Productivity}, author = {Aguirre, Alejandro and @@ -8,6 +25,9 @@ year = {2018}, jh = yes, url = {http://arxiv.org/abs/1802.06283}, + eprint = {1802.06283}, + archivePrefix = {arXiv}, + primaryClass = {cs.PL}, } @unpublished{AH18, @@ -648,7 +668,7 @@ inproceedings{HHRRW14, } @inproceedings{WHE13, - title = {{System} {FC} with Explicit Kind Equality}, + title = {System {FC} with Explicit Kind Equality}, author = {Weirich, Stephanie and Hsu, Justin and Eisenberg, Richard A.}, @@ -772,6 +792,110 @@ inproceedings{HHRRW14, } %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TALKS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +@talk{ucl-pplv18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {{PPLV} Seminar, University College London}, + year = 2018, + month = feb, + jh = yes, +} + +@talk{aachen18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {{UnRAVeL} Seminar, {RWTH} Aachen University}, + year = 2018, + month = feb, + jh = yes, +} + +@talk{imperial18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {Philippa Gardner's Seminar, Imperial College London}, + year = 2018, + month = feb, + jh = yes, +} + +@talk{chocola18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {{CHoCoLa} Seminar, {ENS} Lyon}, + year = 2018, + month = feb, + jh = yes, +} + +@talk{turing18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {Logic Seminar, Alan Turing Institute}, + year = 2018, + month = feb, + jh = yes, +} + +@talk{strathclyde18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {{MSP} Seminar, University of Strathclyde}, + year = 2018, + month = feb, + jh = yes, +} + +@talk{edinburgh18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {{LFCS} Seminar, University of Edinburgh}, + year = 2018, + month = feb, + jh = yes, +} + +@talk{prosecco18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {Prosecco Seminar, Inria Paris}, + year = 2018, + month = jan, + jh = yes, +} + +@talk{pps18-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {{PPS} Seminar, {IRIF}}, + year = 2018, + month = jan, + jh = yes, +} + +@talk{popl18-talk, + title = {Proving Expected Sensitivity of Probabilistic Programs}, + organization = popl18, + year = 2018, + month = jan, + jh = yes, +} + +@talk{oxford17-talk, + title = {From Probabilistic Coupling to Relational Program Logics}, + organization = {Verification Seminar, Oxford University}, + year = 2017, + month = dec, + 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}, + year = 2017, + month = dec, + jh = yes, +} + @talk{icalp17-talk, title = {$\star$-Liftings for Differential Privacy}, organization = icalp17, @@ -869,7 +993,7 @@ inproceedings{HHRRW14, } @talk{wine16-talk, - title = {Computer-aided verification in mechanism design}, + title = {Computer-Aided Verification in Mechanism Design}, organization = wine16, year = 2016, month = dec, @@ -918,7 +1042,7 @@ inproceedings{HHRRW14, @talk{msrc16-talk, title = {Formal Verification of Randomized Algorithms}, - organization = {Constructive Security Seminar, MSR Cambridge UK}, + organization = {Constructive Security Seminar, Microsoft Research Cambridge}, year = 2016, month = jul, jh = yes, @@ -933,8 +1057,8 @@ inproceedings{HHRRW14, } @talk{tpdp16-talk, - title = {Differential Privacy is an Approximate Probabilistic Coupling}, - organization = {Workshop on the Theory and Practice of Differential Privacy (TPDP)}, + title = {Differential Privacy Is an Approximate Probabilistic Coupling}, + organization = {Workshop on the Theory and Practice of Differential Privacy ({TPDP})}, year = 2016, month = jun, jh = yes, @@ -942,7 +1066,7 @@ inproceedings{HHRRW14, @talk{crcs16-talk, title = {Differential Privacy is an Approximate Probabilistic Coupling}, - organization = {CRCS Seminar, Harvard}, + organization = {{CRCS} Seminar, Harvard}, year = 2016, month = jun, jh = yes, @@ -950,15 +1074,15 @@ inproceedings{HHRRW14, @talk{njpls16-talk, title = {A Program Logic for Union Bounds}, - organization = {NJ Programming Languages and Systems Seminar (NJPLS)}, + organization = {NJ Programming Languages and Systems Seminar ({NJPLS})}, year = 2016, month = may, jh = yes, } @talk{uwisc16-talk, - title = {Relational reasoning via probabilistic coupling}, - organization = {PL Seminar, University of Wisconsin}, + title = {Relational Reasoning via Probabilistic Coupling}, + organization = {{PL} Seminar, University of Wisconsin}, year = 2016, month = may, jh = yes, @@ -982,7 +1106,7 @@ inproceedings{HHRRW14, @talk{nsf-sfm15-talk, title = {What Are We Measuring, Anyways?}, - organization = {NSF Workshop on Formal Methods for Information Security}, + organization = {{NSF} Workshop on Formal Methods for Information Security}, year = 2015, month = nov, jh = yes, @@ -998,8 +1122,7 @@ inproceedings{HHRRW14, @talk{shonan15-talk, title = {Language-Based Verification for Differential Privacy}, - organization = {Shonan Meeting on Logic and Verification Methods in Security and - Privacy}, + organization = {Shonan Meeting on Logic and Verification Methods in Security and Privacy}, year = 2015, month = nov, jh = yes, @@ -1039,7 +1162,7 @@ inproceedings{HHRRW14, @talk{cornell15-talk, title = {Verifying Accuracy of Randomized Algorithms}, - organization = {Cornell PL Discussion Group}, + organization = {PL Discussion Group, Cornell University}, year = 2015, month = mar, jh = yes, diff --git a/content/news.md b/content/news.md index 4e46a8c..6ba1a11 100644 --- a/content/news.md +++ b/content/news.md @@ -1,3 +1,5 @@ ++ **03/2018** Our preprint **Probabilistic Program Equivalence for NetKAT** is + now available. + **02/2018** Our preprint **Almost Sure Productivity** is now available. + **02/2018** I will be serving on the program committe of [**LICS 2018**](http://lics.siglog.org/lics18/) in Oxford, England. @@ -15,6 +17,3 @@ **POPL 2018**! + **09/2017** Our preprint **Synthesizing Coupling proofs of Differential Privacy** is now available. -+ **07/2017** Slides now available for **\*-Liftings for Differential Privacy**. -+ **07/2017** Our preprint **Proving Expected Sensitivity of Probabilistic - Programs** is now available.