diff --git a/content/about.md b/content/about.md index 3e1b8ce..7eb136f 100644 --- a/content/about.md +++ b/content/about.md @@ -6,43 +6,41 @@ University](https://www.cornell.edu). **I am always looking for good students!** -Previously, I was a professor in the [Department of Computer +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 was a graduate student in -the [Department of Computer Science](https://cis.upenn.edu) at the [University -of Pennsylvania](https://www.upenn.edu). +[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 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**. +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. -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 +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 that is currently under extensive study. -I have investigated a variety of formal methods---such as [**type +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. +logics**](https://en.wikipedia.org/wiki/Hoare_logic) 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. +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/)