In my research I build theories and systems about programming. A theory tries to understand 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 .
I showed that working memory limits a person's ability to remember the value of variables while program tracing .
I articulated a design space for documentation generators based on a cognitive task analysis of how developers search through APIs .
I demonstrated that machine learning models can classify a program's high-level structure to a high degree of accuracy .
HATRA @ SPLASH 2021.
PLATEAU @ SPLASH 2020.
HATRA @ SPLASH 2020.
PLATEAU @ UIST 2019.
AI Systems @ SOSP 2019.
PLATEAU @ SPLASH 2018.
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!
HashMap. See: willcrichton/lia.
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, 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!