85 lines
4.8 KiB
Markdown
85 lines
4.8 KiB
Markdown
I am an associate professor in the [Department of Computer
|
|
Science](https://www.cs.cornell.edu/) at [Cornell
|
|
University](https://www.cornell.edu).
|
|
|
|
|
|
**I am always looking for good students!**
|
|
|
|
|
|
Previously, I was an assistant professor in the [Department of Computer
|
|
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,
|
|
Logic, and Verification Group](http://pplv.cs.ucl.ac.uk/welcome/) at the
|
|
[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).
|
|
|
|
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
|
|
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 **accuracy**, **incentive compatibility**, Markov chain
|
|
**mixing**, various notions of **algorithmic stability**, and [**differential
|
|
privacy**](https://en.wikipedia.org/wiki/Differential_privacy), a rigorous
|
|
definition of privacy. I have developed a variety of [**type
|
|
systems**](https://en.wikipedia.org/wiki/Type_system) and [**program
|
|
logics**](https://en.wikipedia.org/wiki/Hoare_logic) to verify that programs are
|
|
differentially private.
|
|
|
|
More broadly, I am interested in verifying all kinds of programs and properties
|
|
with rich mathematical structure, such as continuous-time systems, programs with
|
|
symmetries, economic mechanisms, and most recently, algorithms from numerical
|
|
analysis and applied mathematics.
|
|
|
|
## Teaching ##
|
|
- **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/)
|
|
- **Category Theory for Computer Scientists (CS 6117)**: [F22](teaching/f22/cs6117)
|
|
- **Foundations of Probabilistic Programming (CS 6182)**: [F21](teaching/f21/cs6182)
|
|
- **Reasoning about Probabilistic Programs** <br>
|
|
**Invited Course at [OPLSS 2021](https://www.cs.uoregon.edu/research/summerschool/summer21/index.php)**:
|
|
[[slides](https://justinhsu.net/files/slides/oplss21.pdf)] [[recordings](https://www.cs.uoregon.edu/research/summerschool/summer21/topics.php)]
|
|
- **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/)
|
|
- **Topics in Security and Privacy Technologies (CS 839)**: [F18](teaching/f18/cs839/)
|
|
|
|
## 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
|
|
|
|
## 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](https://blog.sigplan.org/blog/)!
|
|
|
|
- [**Teaching Category Theory to Computer Scientists**](https://blog.sigplan.org/2023/04/04/teaching-category-theory-to-computer-scientists/)
|
|
- [**Programming Languages Mentoring Workshop: Ten Years Later**](https://blog.sigplan.org/2021/05/11/programming-languages-mentoring-workshop-ten-years-later/)
|
|
- [**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/)
|