PhD, Computer Science
BS, Computer Science
BS, Molecular & Cellular Biology
Recent & Upcoming Talks
Hazel: Type-Theoretic Foundations for Live Hole-Driven Development
I lead the Hazel project, which has developed a type-theoretic account of live programming with holes, which (1) stand for parts of the program that are not yet fully written, and (2) serve as membranes around type and binding errors.
These papers serve as the foundation for our ongoing research into the future of live programming environments.
Relit + Wyvern: Reasonably Programmable Literal Notation
My thesis research developed mechanisms that allow library providers to install new type-specific literal notation (e.g. SQL literals) while ensuring that client programmers can still reason abstractly and compositionally about types and binding.
Relit implements the mechanism from the ICFP 2018 paper into Reason, which is Facebook's new front-end for OCaml, and the Wyvern programming language implements the mechanism from the ECOOP 2014 paper.
Palettes: Type-Specific User Interfaces for Code Completion
Palettes allow library providers to install new graphical user interfaces that generate code of a specified type at edit-time. We empirically validated our design and gathered a large number of use cases by conducting a survey of 500 developers, then we implemented palettes for Java as an Eclipse extension called Graphite and performed a small pilot study.
Information Theoretic Foundations for Brain-Computer Interfaces
We built a provably optimal EEG-based brain-computer interface by studying the information theoretic properties of noisy asymmetric channels and developing statistical models of user intent for various types of communication/control tasks.
typy: Programmable Semantic Fragments
typy allows library providers to install new statically typed semantic fragments into Python, while leaving its syntax alone (this cleverly sidesteps the "expression problem"). We have applied typy to problems in web security and data science.
SciUnit: Collaborative Infrastructure for Test-Driven Scientific Model Validation
One of the pillars of the scientific method is model validation: comparing a scientific model’s predictions against empirical data. The SciUnit project casts this as a form of collaborative software testing and develops useful infrastructure.
Neurobiological Circuit Dynamics
I entered grad school as a computational neurobiologist. I was interested in how biological circuits process information, so I developed a model of how the excitatory-inhibitory circuitry in the rodent whisker barrel cortex responds to stimulation.