Justin Hsu

Contacts

UCL
Room 3.05
Gower Street 66-72
London WC1E 6BT

Email
email@justinh.su

About Me

I am a postdoc in the Programming Principles, Logic, and Verification Group at the University College London, hosted by Alexandra Silva.

Previously, I was a graduate student in the Department of Computer Science at the University of Pennsylvania, associated with the Theory Group, the PL Club, and the Privacy Group. I was very fortunate to be co-advised by Benjamin Pierce and Aaron Roth.

Research Interests

My research spans two classical areas of computer science: algorithms from theoretical computer science (commonly known as TCS) and formal verification. My work has mostly centered on differential privacy, a rigorous definition of privacy that is currently under extensive study.

From the verification side, I investigate formal methods—such as type systems and program logics—to verify that programs are differentially private. More generally, I consider formal verification for properties of randomized algorithms, including incentive compatibility, Markov chain mixing, and various notions of algorithmic stability. From the algorithms side, I apply differential privacy to optimization, machine learning, and mechanism design.

Service

  • WWW 2018 PC
  • FCS 2017 PC
  • TPDP 2017 PC
  • MFPS 2017 PC
  • PLDI 2016 ERC
News
Bibliography

Drafts

2017
Reasoning about Divergences for Relaxations of Differential Privacy
Tetsuya Sato, Gilles Barthe, Marco Gaboradi, Justin Hsu, and Shin-ya Katsumata.
[Paper]
2017
A Program Logic for Probabilistic Programs
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
[Paper]

Thesis

2017
Probabilistic Couplings for Probabilistic Reasoning
Justin Hsu.
University of Pennsylvania.
[Paper]

Refereed Publications

2018
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi and Justin Hsu.
Proceedings of the ACM on Programming Languages, 2(POPL).
[Paper]
To appear at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Los Angeles, California
2018
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
Proceedings of the ACM on Programming Languages, 2(POPL).
[Paper]
To appear at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Los Angeles, California
2017
Dual Query: Practical Private Query Release for High Dimensional Data
Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Zhiwei Steven Wu.
Journal of Privacy and Confidentiality, 7(2).
[Paper] [Poster]
Previously published in International Conference on Machine Learning (ICML), Beijing, China, 2014.
2017
-Liftings for Differential Privacy
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub.
In International Colloquium on Automata, Languages and Programming (ICALP), Warsaw, Poland.
[Paper] [Slides]
2017
Proving Uniformity and Independence by Self-Composition and Coupling
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Maun, Botswana.
[Paper] [Slides]
2017
Coupling Proofs Are Probabilistic Product Programs
Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France.
[Paper] [Slides]
2017
A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France.
[Paper]
2016
Private Matchings and Allocations
Justin Hsu, Zhiyi Huang, Aaron Roth, Tim Roughgarden, and Zhiwei Steven Wu.
SIAM Journal on Computing, 45(6).
[Paper] [Poster]
Previously published in ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York, 2014.
2016
Computer-Aided Verification in Mechanism Design
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub.
In Conference on Web and Internet Economics (WINE), Montréal, Québec.
[Paper] [Slides]
2016
Advanced Probabilistic Couplings for Differential Privacy
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In ACM SIGSAC Conference on Computer and Communications Security (CCS), Vienna, Austria.
[Paper] [Slides]
2016
Differentially Private Bayesian Programming
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, and Pierre-Yves Strub.
In ACM SIGSAC Conference on Computer and Communications Security (CCS), Vienna, Austria.
[Paper]
2016
Synthesizing Probabilistic Invariants via Doob's Decomposition
Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu.
In International Conference on Computer Aided Verification (CAV), Toronto, Ontario.
[Paper]
2016
A Program Logic for Union Bounds
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy.
[Paper]
2016
Proving Differential Privacy via Probabilistic Couplings
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub.
In IEEE Symposium on Logic in Computer Science (LICS), New York, New York.
[Paper] [Slides]
2016
Do Prices Coordinate Markets?
Justin Hsu, Jamie Morgenstern, Ryan Rogers, Aaron Roth, and Rakesh Vohra.
In ACM SIGACT Symposium on Theory of Computing (STOC), Cambridge, Massachusetts.
[Paper]
2016
Jointly Private Convex Programming
Justin Hsu, Zhiyi Huang, Aaron Roth, and Zhiwei Steven Wu.
In ACM–SIAM Symposium on Discrete Algorithms (SODA), Arlington, Virginia.
[Paper] [Slides]
2016
Programming Language Techniques for Differential Privacy
Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce.
ACM SIGLOG News, 3(1).
[Paper]
2015
Relational Reasoning via Probabilistic Coupling
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub.
In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Suva, Fiji.
[Paper] [Slides]
2015
Online Assignment with Heterogeneous Tasks in Crowdsourcing Markets
Sepehr Assadi, Justin Hsu, and Shahin Jabbari.
In AAAI Conference on Human Computation and Crowdsourcing (HCOMP), San Diego, California.
[Paper]
2015
A Theory AB Toolbox
Marco Gaboardi and Justin Hsu.
In Summit on Advances in Programming Languages (SNAPL), Asilomar, California.
[Paper] [Slides]
2015
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India.
[Paper] [Slides]
2015
Death, Taxes, and Formal Verification (Abstract)
Justin Hsu.
In Summit on Advances in Programming Languages (SNAPL), Asilomar, California.
[Paper] [Slides]
2014
Really Natural Linear Indexed Type-Checking
Arthur Azevedo de Amorim, Marco Gaboardi, Emilio Jesús Gallego Arias, and Justin Hsu.
In Symposium on Implementation and Application of Functional Programming Languages (IFL), Boston, Massachusetts.
[Paper] [Slides]
2014
Proving Differential Privacy in Hoare Logic
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, and Pierre-Yves Strub.
In IEEE Computer Security Foundations Symposium (CSF), Vienna, Austria.
[Paper]
2014
Differential Privacy: An Economic Method for Choosing Epsilon
Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan, Benjamin C. Pierce, and Aaron Roth.
In IEEE Computer Security Foundations Symposium (CSF), Vienna, Austria.
[Paper] [Slides]
2014
Privately Solving Linear Programs
Justin Hsu, Aaron Roth, Tim Roughgarden, and Jonathan Ullman.
In International Colloquium on Automata, Languages and Programming (ICALP), Copenhagen, Denmark.
[Paper] [Slides]
2013
System FC with Explicit Kind Equality
Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.
In ACM SIGPLAN International Conference on Functional Programming (ICFP), Boston, Massachusetts.
[Paper]
2013
Differential Privacy for the Analyst via Private Equilibrium Computation
Justin Hsu, Aaron Roth, and Jonathan Ullman.
In ACM SIGACT Symposium on Theory of Computing (STOC), Palo Alto, California.
[Paper] [Slides]
2013
Linear Dependent Types for Differential Privacy
Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce.
In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy.
[Paper]
2013
Automatic Sensitivity Analysis using Linear Dependent Types
Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, Justin Hsu, and Benjamin C. Pierce.
In International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA), informal proceedings.
[Paper]
2012
Distributed Private Heavy Hitters
Justin Hsu, Sanjeev Khanna, and Aaron Roth.
In International Colloquium on Automata, Languages and Programming (ICALP), Warwick, England.
[Paper] [Slides]
Thanks to Raef Bassily and Adam Smith for spotting an error, now fixed.