Justin Hsu

Contacts

Gates Hall
Ithaca, New York

About Me

I am an assistant professor in the Department of Computer Science at Cornell University.

I am always looking for good students!

Previously, I was an assistant professor in the Department of Computer Sciences at the University of Wisconsin–Madison, and a postdoc at the Department of Computer Science at Cornell University, and in the Programming Principles, Logic, and Verification Group at the University College London. I was a graduate student in the Department of Computer Science at the University of Pennsylvania.

I am funded by an NSF CAREER award and a Facebook Research award.

Research Interests

I design methods to formally verify that programs are correct, especially programs that use randomization. Such programs can be easy to show correct on paper, but surprisingly challenging for computers to analyze. Accordingly, my research blends ideas from two classical areas of computer science: randomized algorithms from theoretical computer science (TCS) and formal verification.

Drawing inspiration from how humans reason about randomized algorithms, we can build simpler and more automated verification techniques. In the past, I’ve applied this approach to properties like accuracy, incentive compatibility, Markov chain mixing, and various notions of algorithmic stability.

A particular focus of my work has been differential privacy, a rigorous definition of privacy that is currently under extensive study. I have investigated a variety of formal methods—such as type systems and program logics—to verify that programs are differentially private.

From a more traditional algorithms perspective, I am also interested in applying differential privacy to optimization, machine learning, and mechanism design.

Teaching

Category Theory for Computer Scientists (CS 6117): F22
Data Structures and Functional Programming (CS 3110): S22
Foundations of Probabilistic Programming (CS 6182): F21
Reasoning about Probabilistic Programs
Invited Course at OPLSS 2021: [slides] [recordings]
Security and Privacy in Data Science (CS 763): F20
Introduction to the Theory and Design of PL (CS 538): S20
Security and Privacy in Data Science (CS 763): F19
Introduction to the Theory and Design of PL (CS 538): S19
Topics in Security and Privacy Technologies (CS 839): F18

Service

2023 CSF, ICALP-B, LICS, OOPSLA, MFPS
2022 POPL, PLDI, MFPS (co-chair)
2021 ESOP, , CSF, AAAI, COLT, WoLLIC, MFPS
2020 AAAI, CSF, LAFI, WoLLIC, , OOPSLA (ERC)
2019 POPL, , POST, CSF, DARS (co-chair)
2018 LICS, WWW
2017 FCS, TPDP, MFPS
2016 PLDI (ERC)

Blogging

I’ve greatly enjoyed blogging for PL Perspectives!

Verifying Randomized Algorithms: Why and How?
Re-Imagining the “Programming Paradigms” Course
Programming Languages Mentoring Workshop: Ten Years Later

News

08/2022 Our paper Data-Driven Invariant Learning for Probabilistic Programs received a Distinguished Paper Award at CAV 2022!
08/2022 This fall, I am teaching Category Theory for Computer Scientists (CS 6117)!
07/2022 Symbolic Execution for Randomized Programs to appear at OOPSLA 2022.
05/2022 Data-Driven Invariant Learning for Probabilistic Programs to appear at CAV 2022.
02/2022 P4BID: Information Flow Control in P4 to appear at PLDI 2022.
01/2022 I will be co-chairing MFPS 38 with Christine Tasson, planned to be hybrid with an in-person meeting in Ithaca, New York. Submit your best papers!
01/2022 This spring, I am co-teaching 🐫Data Structures and Functional Programming (CS 3110)🐫 with Nate Foster.
11/2021 A Separation Logic for Negative Dependence to appear at POPL 2022.

Bibliography

Drafts

2022	An abstract approach to conditional independence in DIBI models Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi.

Thesis

2017	Probabilistic Couplings for Probabilistic Reasoning [Paper] Justin Hsu. University of Pennsylvania. Selected for the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award

Invited Chapters and Surveys

2020	Probabilistic Couplings from Program Logics [Paper] Gilles Barthe and Justin Hsu. In Foundations of Probabilistic Programming Languages.
2016	Programming Language Techniques for Differential Privacy [Paper] Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. ACM SIGLOG News, 3(1).

Refereed Publications

2022	Symbolic Execution for Randomized Programs [Paper] Zachary Susag, Sumit Lahiri, Justin Hsu, and Subhajit Roy. Proceedings of the ACM on Programming Languages, 6(OOPSLA). Appeared at ACM SIGPLAN Conference on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), Auckland, New Zealand.
2022	Data-Driven Invariant Learning for Probabilistic Programs [Paper] Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. In International Conference on Computer Aided Verification (CAV), Haifa, Israel. Distinguished Paper Award.
2022	P4BID: Information Flow Control in P4 [Paper] Karuna Grewal, Loris D’Antoni, and Justin Hsu. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), San Diego, California.
2022	A Separation Logic for Negative Dependence [Paper] Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti. Proceedings of the ACM on Programming Languages, 6(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania.
2021	A Bunched Logic for Conditional Independence [Paper] Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. In ACM/IEEE Symposium on Logic in Computer Science (LICS).
2021	A Quantum Interpretation of Bunched Logic & Quantum Separation Logic [Paper] Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. In ACM/IEEE Symposium on Logic in Computer Science (LICS).
2021	Learning Differentially Private Mechanisms [Paper] Subhajit Roy, Justin Hsu, and Aws Albarghouthi. In IEEE Symposium on Security and Privacy (S&P).
2021	A Pre-Expectation Calculus for Probabilistic Sensitivity [Slides] [Paper] Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Proceedings of the ACM on Programming Languages, 5(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL). Distinguished Paper Award.
2020	Hypothesis Testing Interpretations and Rényi Differential Privacy [Paper] Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Tetsuya Sato. In International Conference on Artificial Intelligence and Statistics (AISTATS), Palermo, Italy.
2020	A Probabilistic Separation Logic [Paper] Gilles Barthe, Justin Hsu, and Kevin Liao. Proceedings of the ACM on Programming Languages, 4(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana.
2020	Guarded Kleene Algebra with Tests [Paper] Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Proceedings of the ACM on Programming Languages, 4(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana. Distinguished Paper Award.
2020	Relational Proofs for Quantum Programs [Paper] Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. Proceedings of the ACM on Programming Languages, 4(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana.
2019	Relational ⋆-Liftings for Differential Privacy [Slides] [Paper] Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub. Logical Methods in Computer Science, 15(4). Previously published in International Colloquium on Automata, Languages and Programming (ICALP), Warsaw, Poland, 2017.
2019	Data Poisoning against Differentially-Private Learners: Attacks and Defenses [Paper] Yuzhe Ma, Xiaojin Zhu, and Justin Hsu. In International Joint Conference on Artificial Intelligence (IJCAI), Macao, China.
2019	Probabilistic Relational Reasoning via Metrics [Paper] Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. In IEEE Symposium on Logic in Computer Science (LICS), Vancouver, British Columbia.
2019	Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy [Paper] Tetsuya Sato, Gilles Barthe, Marco Gaboradi, Justin Hsu, and Shin-ya Katsumata. In IEEE Symposium on Logic in Computer Science (LICS), Vancouver, British Columbia.
2019	Scalable Verification of Probabilistic Network Programs [Paper] Steffen Smolka, Praveen Kumar, David M Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Phoenix, Arizona.
2019	Trace Abstraction modulo Probability [Paper] Calvin Smith, Justin Hsu, and Aws Albarghouthi. Proceedings of the ACM on Programming Languages, 3(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Lisbon, Portugal.
2019	Formal Verification of Higher-Order Probabilistic Programs [Paper] Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu. Proceedings of the ACM on Programming Languages, 3(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Lisbon, Portugal.
2018	Convex Language Semantics for Nondeterministic Probabilistic Automata [Paper] Gerco van Heerdt, Justin Hsu, Joël Ouaknine, and Alexandra Silva. In International Colloquium on Theoretical Aspects of Computing (ICTAC), Stellenbosch, South Africa.
2018	Constraint-Based Synthesis of Coupling Proofs [Paper] Aws Albarghouthi and Justin Hsu. In International Conference on Computer Aided Verification (CAV), Oxford, England.
2018	Almost Sure Productivity [Paper] Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva. In International Colloquium on Automata, Languages and Programming (ICALP), Prague, Czech Republic.
2018	An Assertion-Based Program Logic for Probabilistic Programs [Slides] [Paper] Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. In European Symposium on Programming (ESOP), Thessaloniki, Greece.
2018	Synthesizing Coupling Proofs of Differential Privacy [Paper] Aws Albarghouthi and Justin Hsu. Proceedings of the ACM on Programming Languages, 2(POPL). Appeared at ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Los Angeles, California.
2018	Proving Expected Sensitivity of Probabilistic Programs [Slides] [Paper] Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. Proceedings of the ACM on Programming Languages, 2(POPL). Appeared 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 [Poster] [Paper] Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Zhiwei Steven Wu. Journal of Privacy and Confidentiality, 7(2). Previously published in International Conference on Machine Learning (ICML), Beijing, China, 2014.
2017	Proving Uniformity and Independence by Self-Composition and Coupling [Slides] [Paper] 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.
2017	Coupling Proofs Are Probabilistic Product Programs [Slides] [Paper] Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France.
2017	A Semantic Account of Metric Preservation [Paper] 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.
2016	Private Matchings and Allocations [Poster] [Paper] Justin Hsu, Zhiyi Huang, Aaron Roth, Tim Roughgarden, and Zhiwei Steven Wu. SIAM Journal on Computing, 45(6). Previously published in ACM SIGACT Symposium on Theory of Computing (STOC), New York, New York, 2014.
2016	Computer-Aided Verification in Mechanism Design [Slides] [Paper] 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.
2016	Advanced Probabilistic Couplings for Differential Privacy [Slides] [Paper] 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. There is an error in the treatment of advanced composition; please see my thesis for the correction.
2016	Differentially Private Bayesian Programming [Paper] 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.
2016	Synthesizing Probabilistic Invariants via Doob’s Decomposition [Paper] Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu. In International Conference on Computer Aided Verification (CAV), Toronto, Ontario.
2016	A Program Logic for Union Bounds [Paper] Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. In International Colloquium on Automata, Languages and Programming (ICALP), Rome, Italy.
2016	Proving Differential Privacy via Probabilistic Couplings [Slides] [Paper] 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.
2016	Do Prices Coordinate Markets? [Paper] Justin Hsu, Jamie Morgenstern, Ryan Rogers, Aaron Roth, and Rakesh Vohra. In ACM SIGACT Symposium on Theory of Computing (STOC), Cambridge, Massachusetts.
2016	Jointly Private Convex Programming [Slides] [Paper] Justin Hsu, Zhiyi Huang, Aaron Roth, and Zhiwei Steven Wu. In ACM–SIAM Symposium on Discrete Algorithms (SODA), Arlington, Virginia.
2015	Relational Reasoning via Probabilistic Coupling [Slides] [Paper] 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.
2015	Online Assignment with Heterogeneous Tasks in Crowdsourcing Markets [Paper] Sepehr Assadi, Justin Hsu, and Shahin Jabbari. In AAAI Conference on Human Computation and Crowdsourcing (HCOMP), San Diego, California.
2015	A Theory AB Toolbox [Slides] [Paper] Marco Gaboardi and Justin Hsu. In Summit on Advances in Programming Languages (SNAPL), Asilomar, California.
2015	Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy [Slides] [Paper] 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.
2014	Really Natural Linear Indexed Type-Checking [Slides] [Paper] 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.
2014	Proving Differential Privacy in Hoare Logic [Paper] 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.
2014	Differential Privacy: An Economic Method for Choosing Epsilon [Slides] [Paper] 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.
2014	Privately Solving Linear Programs [Slides] [Paper] Justin Hsu, Aaron Roth, Tim Roughgarden, and Jonathan Ullman. In International Colloquium on Automata, Languages and Programming (ICALP), Copenhagen, Denmark.
2013	System FC with Explicit Kind Equality [Paper] Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Boston, Massachusetts.
2013	Differential Privacy for the Analyst via Private Equilibrium Computation [Slides] [Paper] Justin Hsu, Aaron Roth, and Jonathan Ullman. In ACM SIGACT Symposium on Theory of Computing (STOC), Palo Alto, California.
2013	Linear Dependent Types for Differential Privacy [Paper] 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.
2012	Distributed Private Heavy Hitters [Slides] [Paper] Justin Hsu, Sanjeev Khanna, and Aaron Roth. In International Colloquium on Automata, Languages and Programming (ICALP), Warwick, England. Thanks to Raef Bassily and Adam Smith for spotting an error, now fixed.