Contacts

Gates Hall
Ithaca, New York
email@justinh.su
email@justinhsu.net

About Me

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

This year, I am away on sabbatical at Imperial College London. I will be back to Cornell in August 2025.

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 obtained my PhD from the Department of Computer Science at the University of Pennsylvania.

I am funded by the National Science Foundation, the Office of Naval Research, and Facebook Research.

Research Interests

I design methods to formally verify that algorithms are correct. I am especially interested in programs satisfying quantitative guarantees, or other properties from mathematical or scientific applications.

A particular focus of my work has been verifying programs that use randomization. Such programs can be easy to show correct on paper, but surprisingly challenging for computers to analyze. 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 statistical accuracy, incentive compatibility, Markov chain mixing, algorithmic stability, and differential privacy.

More broadly, I am interested in verification for all kinds of programs with rich mathematical structure and properties, such as continuous-time systems, programs with symmetries, economic mechanisms, runtime monitors for hierarchical policies, and algorithms from numerical analysis and applied mathematics.

Teaching

  • Data Structures and Functional Programming (CS 3110): F23 S23 S22
  • Category Theory for Computer Scientists (CS 6117): F22
  • 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 F19
  • Introduction to the Theory and Design of PL (CS 538): S20 S19
  • Topics in Security and Privacy Technologies (CS 839): F18

Awards and Honors

Service

  • 2024 OOPSLA, CSF, CCS, MFPS
  • 2023 CSF, ICALP-B, LICS, OOPSLA, MFPS
  • 2022 POPL, PLDI, MFPS (co-chair)
  • 2021 ESOP, PLMW@POPL, CSF, AAAI, COLT, WoLLIC, MFPS
  • 2020 AAAI, CSF, LAFI, WoLLIC, PLMW@POPL, OOPSLA (ERC)
  • 2019 POPL, PLMW@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!

News
Bibliography

Drafts

2023 Separated and Shared Effects in Higher-Order Languages [Paper]
Pedro H. Azevedo de Amorim and Justin Hsu.

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

2024 Numerical Fuzz: A Type System for Rounding Error Analysis [Paper]
Ariel E. Kellison and Justin Hsu.
Proceedings of the ACM on Programming Languages, 8(PLDI).
Appeared at ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Copenhagen, Denmark.
2024 Data-Driven Invariant Learning for Probabilistic Programs [Paper]
Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy.
Formal Methods in System Design.
Previously published in International Conference on Computer Aided Verification (CAV), Haifa, Israel, 2022.
2024 A Categorical Approach to DIBI Models [Paper]
Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi.
In International Conference on Formal Structures for Computation and Deduction (FSCD), Tallinn, Estonia.
2024 Verifying Cake-Cutting, Faster [Paper]
Noah Bertram, Tean Lai, and Justin Hsu.
In International Conference on Computer Aided Verification (CAV), Montréal, Québec.
2023 Expressive Policies for Microservice Networks [Paper]
Karuna Grewal, Brighten Godfrey, and Justin Hsu.
In ACM Workshop on Hot Topics in Networks (HotNets), Cambridge, Massachusetts.
2023 Cutting the Cake: A Language for Fair Division [Paper]
Noah Bertram, Alex Levinson, and Justin Hsu.
Proceedings of the ACM on Programming Languages, 7(PLDI).
Appeared at ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Orlando, Florida.
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 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.