2024-07-15 23:05:02 +00:00
I am an associate professor in the [Department of Computer
2021-07-16 22:12:58 +00:00
Science](https://www.cs.cornell.edu/) at [Cornell
University](https://www.cornell.edu).
2018-09-03 06:46:31 +00:00
2024-09-02 14:57:49 +00:00
**This year, I am away on sabbatical at Imperial College London. I will be back to Cornell in August 2025.**
2018-09-03 06:46:31 +00:00
2024-07-19 04:57:54 +00:00
Previously, I was an assistant professor in the [Department of Computer
2021-07-16 22:12:58 +00:00
Sciences](https://www.cs.wisc.edu/) at the [University of
Wisconsin--Madison](https://www.wisc.edu), and a postdoc at the [Department of
Computer Science](https://www.cs.cornell.edu/) at [Cornell
University](https://www.cornell.edu/), and in the [Programming Principles,
2018-09-03 06:46:31 +00:00
Logic, and Verification Group](http://pplv.cs.ucl.ac.uk/welcome/) at the
2024-07-19 04:57:54 +00:00
[University College London ](https://www.ucl.ac.uk/ ). I obtained my PhD from the
[Department of Computer Science ](https://cis.upenn.edu ) at the [University of
Pennsylvania](https://www.upenn.edu).
2015-08-17 10:10:24 +00:00
2023-01-10 23:09:20 +00:00
I am funded by the National Science Foundation, the Office of Naval Research,
and Facebook Research.
2020-05-01 21:15:43 +00:00
2015-01-05 04:43:45 +00:00
## Research Interests ##
2024-07-19 04:57:54 +00:00
I design methods to **formally verify** that **algorithms** are correct. I am
2024-07-19 05:15:51 +00:00
especially interested in programs satisfying quantitative guarantees, or other
2024-07-19 04:57:54 +00:00
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
2024-07-19 05:15:51 +00:00
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,
2024-07-19 05:23:30 +00:00
programs with symmetries, economic mechanisms, runtime monitors for hierarchical
policies, and algorithms from numerical analysis and applied mathematics.
2017-01-17 10:33:57 +00:00
2018-09-05 03:51:09 +00:00
## Teaching ##
2023-12-02 05:06:11 +00:00
- **Data Structures and Functional Programming (CS 3110)**: [F23 ](https://www.cs.cornell.edu/courses/cs3110/2023fa/ ) [S23 ](https://www.cs.cornell.edu/courses/cs3110/2023sp/ ) [S22 ](https://www.cs.cornell.edu/courses/cs3110/2022sp/ )
2023-03-30 03:35:53 +00:00
- **Category Theory for Computer Scientists (CS 6117)**: [F22 ](teaching/f22/cs6117 )
2022-08-03 14:31:15 +00:00
- **Foundations of Probabilistic Programming (CS 6182)**: [F21 ](teaching/f21/cs6182 )
2021-07-10 23:35:58 +00:00
- **Reasoning about Probabilistic Programs** < br >
**Invited Course at [OPLSS 2021](https://www.cs.uoregon.edu/research/summerschool/summer21/index.php)** :
2022-11-07 18:41:25 +00:00
[[slides ](https://justinhsu.net/files/slides/oplss21.pdf )] [[recordings ](https://www.cs.uoregon.edu/research/summerschool/summer21/topics.php )]
2023-01-10 23:11:39 +00:00
- **Security and Privacy in Data Science (CS 763)**: [F20 ](teaching/f20/cs763/ ) [F19 ](teaching/f19/cs763/ )
- **Introduction to the Theory and Design of PL (CS 538)**: [S20 ](teaching/s20/cs538/ ) [S19 ](teaching/s19/cs538/ )
2021-01-14 16:55:18 +00:00
- **Topics in Security and Privacy Technologies (CS 839)**: [F18 ](teaching/f18/cs839/ )
2018-09-05 03:51:09 +00:00
2024-07-15 22:10:02 +00:00
## Awards and Honors ##
- **2024** EATCS [Presburger Award ](https://www.eatcs.org/index.php/presburger )
- **2024** Royal Society [Wolfson Visiting Fellowship ](https://royalsociety.org/grants/royal-society-wolfson-visiting-fellowship/ )
- **2022** CAV Distinguished Paper Award
- **2021** POPL Distinguished Paper Award
- **2020** POPL Distinguished Paper Award
- **2020** NSF CAREER award
- **2018** ACM SIGPLAN [John C. Reynolds Doctoral Dissertation Award ](https://www.sigplan.org/Awards/Dissertation/ )
- **2015** Simons Award for Graduate Students in Theoretical Computer Science
2017-01-17 10:33:57 +00:00
## Service ##
2023-12-29 19:38:40 +00:00
- **2024** OOPSLA, CSF, CCS, MFPS
2022-09-30 15:52:00 +00:00
- **2023** CSF, ICALP-B, LICS, OOPSLA, MFPS
2022-03-01 05:06:48 +00:00
- **2022** POPL, PLDI, MFPS (co-chair)
2021-04-01 22:14:17 +00:00
- **2021** ESOP, PLMW@POPL, CSF, AAAI, COLT, WoLLIC, MFPS
2020-05-18 17:24:05 +00:00
- **2020** AAAI, CSF, LAFI, WoLLIC, PLMW@POPL, OOPSLA (ERC)
2020-02-04 21:27:50 +00:00
- **2019** POPL, PLMW@POPL, POST, CSF, DARS (co-chair)
2018-05-25 20:37:57 +00:00
- **2018** LICS, WWW
- **2017** FCS, TPDP, MFPS
- **2016** PLDI (ERC)
2021-07-10 22:41:56 +00:00
## Blogging ##
2021-07-19 17:33:49 +00:00
I've greatly enjoyed blogging for [PL Perspectives ](https://blog.sigplan.org/blog/ )!
2021-07-10 22:41:56 +00:00
2023-04-05 23:03:39 +00:00
- [**Teaching Category Theory to Computer Scientists** ](https://blog.sigplan.org/2023/04/04/teaching-category-theory-to-computer-scientists/ )
2021-07-19 17:33:49 +00:00
- [**Programming Languages Mentoring Workshop: Ten Years Later** ](https://blog.sigplan.org/2021/05/11/programming-languages-mentoring-workshop-ten-years-later/ )
2023-12-02 05:05:11 +00:00
- [**Re-Imagining the “Programming Paradigms” Course** ](https://blog.sigplan.org/2021/01/28/re-imagining-the-programming-paradigms-course/ )
- [**Verifying Randomized Algorithms: Why and How?** ](https://blog.sigplan.org/2020/10/20/verifying-randomized-algorithms-why-and-how/ )
