Tighten up bio.

content/about.md

@@ -1,28 +1,28 @@
-I am a graduate student in the [Department of Computer
+I am a final-year graduate student in the [Department of Computer
 Science](http://cis.upenn.edu) at the [University of
-Pennsylvania](http://www.upenn.edu).  There, I am associated with the [Theory
+Pennsylvania](http://www.upenn.edu), where I am associated with the [Theory
 Group](http://theory.cis.upenn.edu), the [PL
 Club](http://www.cis.upenn.edu/~plclub/), and the [Privacy
 Group](http://privacy.cis.upenn.edu).  I am very fortunate to be co-advised by
 [Benjamin Pierce](http://cis.upenn.edu/~bcpierce) and [Aaron
-Roth](http://cis.upenn.edu/~aaroth). 
-
-I am supported by the Simons Graduate Fellowship in Theoretical Computer
-Science. Previously, I was awarded an Honorable Mention for the NSF Graduate
-Research Fellowship Program.
+Roth](http://cis.upenn.edu/~aaroth). I am partially supported by a Simons
+Graduate Fellowship in Theoretical Computer Science.
 
 ## Research Interests ##
-I spend my time thinking about questions in **verification**, **programming
-languages**, and **algorithms**. My work has mostly centered on [**differential
+My research spans two classical areas of computer science: **algorithms** from
+theoretical computer science (commonly known as **TCS**) and **formal
+verification**. My work has mostly centered on [**differential
 privacy**](http://en.wikipedia.org/wiki/Differential_privacy), a rigorous
 definition of privacy that is currently under extensive study.
 
-From the verification side, I am interested in using formal methods---such as
-[**type systems**](http://en.wikipedia.org/wiki/Type_system) and [**program
-logics**](http://en.wikipedia.org/wiki/Hoare_logic)---to verify that programs are
-differentially private. From the algorithms side, I am interested in
-applications of differential privacy to optimization, machine learning, and
-mechanism design.
+From the verification side, I investigate formal methods---such as [**type
+systems**](http://en.wikipedia.org/wiki/Type_system) and [**program
+logics**](http://en.wikipedia.org/wiki/Hoare_logic)---to verify that programs
+are differentially private. More generally, I consider formal verification for
+properties of randomized algorithms, including **incentive compatibility**,
+Markov chain **mixing**, and various notions of **algorithmic stability**.  From
+the algorithms side, I apply differential privacy to optimization, machine
+learning, and mechanism design.
 
 ## Service ##
 - **TPDP 2017** PC