Add equivalence for probabilistic NetKAT draft.

This commit is contained in:
Justin Hsu 2018-03-27 22:36:09 -04:00
parent 0abe04e7c3
commit 87cbe4ad7d
3 changed files with 144 additions and 18 deletions

View File

@ -200,6 +200,7 @@
@STRING{icfp96 = icfp # ", Philadelphia, Pennsylvania" } @STRING{icfp96 = icfp # ", Philadelphia, Pennsylvania" }
% ---- % ----
@STRING{itp = "Interactive Theorem Proving ({ITP})"} @STRING{itp = "Interactive Theorem Proving ({ITP})"}
@STRING{itp10 = itp # ", Edinburgh, Scotland" }
@STRING{itp11 = itp # ", Nijmegen, The Netherlands" } @STRING{itp11 = itp # ", Nijmegen, The Netherlands" }
@STRING{itp13 = itp # ", Rennes, France" } @STRING{itp13 = itp # ", Rennes, France" }
% ---- % ----
@ -231,6 +232,7 @@
@STRING{oopsla90 = oopslapre96 # "/" # ecoop # ", Ottawa, Ontario" } @STRING{oopsla90 = oopslapre96 # "/" # ecoop # ", Ottawa, Ontario" }
@STRING{oopsla98 = oopsla # ", Vancouver, British Columbia" } @STRING{oopsla98 = oopsla # ", Vancouver, British Columbia" }
@STRING{oopsla03 = oopsla # ", Anaheim, California" } @STRING{oopsla03 = oopsla # ", Anaheim, California" }
@STRING{oopsla13 = oopsla # ", Indianapolis, Indiana" }
@STRING{oopsla14 = oopsla # ", Portland, Oregon" } @STRING{oopsla14 = oopsla # ", Portland, Oregon" }
% ---- % ----
@STRING{lics = "{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS})" } @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{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{stoc82 = stoc # ", San Francisco, California"}
@STRING{stoc83 = stoc # ", Boston, Massachusetts"} @STRING{stoc83 = stoc # ", Boston, Massachusetts"}
@STRING{stoc87 = stoc # ", New York, New York"} @STRING{stoc87 = stoc # ", New York, New York"}
@ -608,8 +612,8 @@
Application of Cryptology and Information Security (ASIACRYPT)" } Application of Cryptology and Information Security (ASIACRYPT)" }
@STRING{ascrypt15 = ascrypt # ", Auckland, New Zealand" } @STRING{ascrypt15 = ascrypt # ", Auckland, New Zealand" }
%---- %----
@STRING{asplos14 = aplas # ", Salt Lake City, Utah" } @STRING{asplos14 = asplos # ", Salt Lake City, Utah" }
@STRING{asplos06 = aplas # ", San Jose, California" } @STRING{asplos06 = asplos # ", San Jose, California" }
%---- %----
@STRING{ceemas07 = ceemas # ", Leipzig, Germany" } @STRING{ceemas07 = ceemas # ", Leipzig, Germany" }
% --- % ---

View File

@ -1,4 +1,21 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%% UNPUBLISHED %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%% 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, @unpublished{ABHS18,
title = {Almost Sure Productivity}, title = {Almost Sure Productivity},
author = {Aguirre, Alejandro and author = {Aguirre, Alejandro and
@ -8,6 +25,9 @@
year = {2018}, year = {2018},
jh = yes, jh = yes,
url = {http://arxiv.org/abs/1802.06283}, url = {http://arxiv.org/abs/1802.06283},
eprint = {1802.06283},
archivePrefix = {arXiv},
primaryClass = {cs.PL},
} }
@unpublished{AH18, @unpublished{AH18,
@ -648,7 +668,7 @@ inproceedings{HHRRW14,
} }
@inproceedings{WHE13, @inproceedings{WHE13,
title = {{System} {FC} with Explicit Kind Equality}, title = {System {FC} with Explicit Kind Equality},
author = {Weirich, Stephanie and author = {Weirich, Stephanie and
Hsu, Justin and Hsu, Justin and
Eisenberg, Richard A.}, Eisenberg, Richard A.},
@ -772,6 +792,110 @@ inproceedings{HHRRW14,
} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TALKS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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, @talk{icalp17-talk,
title = {$\star$-Liftings for Differential Privacy}, title = {$\star$-Liftings for Differential Privacy},
organization = icalp17, organization = icalp17,
@ -869,7 +993,7 @@ inproceedings{HHRRW14,
} }
@talk{wine16-talk, @talk{wine16-talk,
title = {Computer-aided verification in mechanism design}, title = {Computer-Aided Verification in Mechanism Design},
organization = wine16, organization = wine16,
year = 2016, year = 2016,
month = dec, month = dec,
@ -918,7 +1042,7 @@ inproceedings{HHRRW14,
@talk{msrc16-talk, @talk{msrc16-talk,
title = {Formal Verification of Randomized Algorithms}, title = {Formal Verification of Randomized Algorithms},
organization = {Constructive Security Seminar, MSR Cambridge UK}, organization = {Constructive Security Seminar, Microsoft Research Cambridge},
year = 2016, year = 2016,
month = jul, month = jul,
jh = yes, jh = yes,
@ -933,8 +1057,8 @@ inproceedings{HHRRW14,
} }
@talk{tpdp16-talk, @talk{tpdp16-talk,
title = {Differential Privacy is an Approximate Probabilistic Coupling}, title = {Differential Privacy Is an Approximate Probabilistic Coupling},
organization = {Workshop on the Theory and Practice of Differential Privacy (TPDP)}, organization = {Workshop on the Theory and Practice of Differential Privacy ({TPDP})},
year = 2016, year = 2016,
month = jun, month = jun,
jh = yes, jh = yes,
@ -942,7 +1066,7 @@ inproceedings{HHRRW14,
@talk{crcs16-talk, @talk{crcs16-talk,
title = {Differential Privacy is an Approximate Probabilistic Coupling}, title = {Differential Privacy is an Approximate Probabilistic Coupling},
organization = {CRCS Seminar, Harvard}, organization = {{CRCS} Seminar, Harvard},
year = 2016, year = 2016,
month = jun, month = jun,
jh = yes, jh = yes,
@ -950,15 +1074,15 @@ inproceedings{HHRRW14,
@talk{njpls16-talk, @talk{njpls16-talk,
title = {A Program Logic for Union Bounds}, 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, year = 2016,
month = may, month = may,
jh = yes, jh = yes,
} }
@talk{uwisc16-talk, @talk{uwisc16-talk,
title = {Relational reasoning via probabilistic coupling}, title = {Relational Reasoning via Probabilistic Coupling},
organization = {PL Seminar, University of Wisconsin}, organization = {{PL} Seminar, University of Wisconsin},
year = 2016, year = 2016,
month = may, month = may,
jh = yes, jh = yes,
@ -982,7 +1106,7 @@ inproceedings{HHRRW14,
@talk{nsf-sfm15-talk, @talk{nsf-sfm15-talk,
title = {What Are We Measuring, Anyways?}, 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, year = 2015,
month = nov, month = nov,
jh = yes, jh = yes,
@ -998,8 +1122,7 @@ inproceedings{HHRRW14,
@talk{shonan15-talk, @talk{shonan15-talk,
title = {Language-Based Verification for Differential Privacy}, title = {Language-Based Verification for Differential Privacy},
organization = {Shonan Meeting on Logic and Verification Methods in Security and organization = {Shonan Meeting on Logic and Verification Methods in Security and Privacy},
Privacy},
year = 2015, year = 2015,
month = nov, month = nov,
jh = yes, jh = yes,
@ -1039,7 +1162,7 @@ inproceedings{HHRRW14,
@talk{cornell15-talk, @talk{cornell15-talk,
title = {Verifying Accuracy of Randomized Algorithms}, title = {Verifying Accuracy of Randomized Algorithms},
organization = {Cornell PL Discussion Group}, organization = {PL Discussion Group, Cornell University},
year = 2015, year = 2015,
month = mar, month = mar,
jh = yes, jh = yes,

View File

@ -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** Our preprint **Almost Sure Productivity** is now available.
+ **02/2018** I will be serving on the program committe of [**LICS + **02/2018** I will be serving on the program committe of [**LICS
2018**](http://lics.siglog.org/lics18/) in Oxford, England. 2018**](http://lics.siglog.org/lics18/) in Oxford, England.
@ -15,6 +17,3 @@
**POPL 2018**! **POPL 2018**!
+ **09/2017** Our preprint **Synthesizing Coupling proofs of Differential + **09/2017** Our preprint **Synthesizing Coupling proofs of Differential
Privacy** is now available. 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.