Gates Hall
Ithaca, New York
email@justinh.su
email@justinhsu.net
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.
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.
I’ve greatly enjoyed blogging for PL Perspectives!
2023 |
Separated and Shared Effects in Higher-Order Languages
[Paper]
Pedro H. Azevedo de Amorim and Justin Hsu. |
2017 |
Probabilistic Couplings for Probabilistic Reasoning
[Paper]
Justin Hsu. University of Pennsylvania. Selected for the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award |
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). |
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 |
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 |
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. |