I am a computer scientist that designs principled, practical systems to amplify the intelligence of programmers. My research spans programming languages (PL) and human-computer interaction (HCI) with influences from system design, cognitive psychology, and learning science.
I am currently a postdoc at Brown University advised by Shriram Krishnamurthi, working on making Rust easier to learn. I completed my Ph.D. at Stanford University advised by Pat Hanrahan and Maneesh Agrawala.
In my research, I build theories and systems about programming. A theory examines a concept in a simplified setting where its properties can be identified via logical or statistical analysis. A system applies theory to a real-world setting where unexpected constraints and engineering concerns influence the theory's application.
I developed an algorithm for using ownership types to statically & modularly analyze information flow, and proved its soundness as noninterference [4].
I ran experiments that demonstrated how working memory limits a person's ability to remember the value of variables while program tracing [6].
I articulated a design space for documentation generators based on the information needs of developers [9].
I demonstrated that machine learning models can accurately classify a program's high-level structure [7].
I built Flowistry, a static information flow analysis for Rust, to help programmers identify code unrelated to their current task [4].
I redesigned CS 242, a graduate-level course on programming languages, to help students better understand how PL theory works in the real world [12].
I extended Rustdoc to help programmers learn new APIs by automatically linking documentation to code examples.
AI Systems @ SOSP 2019 .
Here are some ideas that I worked on a bit, but haven't had time to keep exploring. If any of them are exciting to you, please reach out and I would love to chat!
Vec
or HashMap
. See: Gradual Programming,
Rust: The New LLVMand willcrichton/lia.
for humans. How can we quantify the concept of
direct mapping? For example, I created the Expressiveness Benchmark as a first pass on this question for tabular data processing APIs. Here's a really cool idea: imagine if you (1) embedded a bunch of APIs into a theorem prover, (2) implemented the same task in each API, and (3) wrote a proof of correctness for each implementation. Does the smallest proof corresponds to the most direct mapping?
Partial evaluation as an aid to the comprehension of Fortran programsand
Amorphous program slicing.
design patternsshould be articulated in terms of these kinds of components, not stuff like a
visitor. For example, I wrote a mini-book Type-Driven API Design in Rust that shows how to idiomatically express system components in Rust, and what mistakes you can catch at compile-time with careful design. But I think a more systematic enumeration of these kinds of system idioms would be really interesting. See also: domain-driven design.
The Role of Working Memory in Program Tracing[6], I explored the idea of modeling a person as a
lossyinterpreter, and whether you could tune the lossiness parameters to explain the range of observed human traces. The models actually worked, although I never figured out what a useful application of such a cognitive model would be. Maybe you can!