Hazelnut: A Bidirectionally Typed Structure Editor Calculus
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)
Tedium-reducing editor services frequently encounter, and balk at, incomplete programs: programs with holes and type inconsistencies. This paper starts from type-theoretic first principles to develop a type system for incomplete programs. It then defines a calculus of type-aware structured edit actions, and proves, using the Agda proof assistant, several powerful theorems about this calculus.
This work lays the foundation for Hazel, the typed lab notebook environment that we are building. Our vision for Hazel is described in the SNAPL 2017 paper below.
Programmable Semantic Fragments: The Design and Implementation of typy
15th International Conference on Generative Programming: Concepts & Experience (GPCE 2016)
Sometimes, reducing tedium requires defining a new semantic fragment. Consider, for example, adding functional record update to ML, or defining a typed FFI to a different language, like OpenCL.
This paper develops a simple system for modularly defining new semantic fragments like these and shows that this system can be embedded into Python as a library, typy.
Safely Composable Type-Specific Languages
28th European Conference on Object-Oriented Programming (ECOOP 2014)
Distinguished Paper Award
This paper describes a simplified variant of my thesis work, and gathers some data to show that "stringly-typed programming" is common in practice.
Active Code Completion
34th International Conference on Software Engineering (ICSE 2012)
In this paper, we describe and empirically evaluate an editor service that allows library providers to associate code generation UIs with type definitions. Clients invoke these UIs via the type-directed code completion menu (our implementation is in Eclipse.)
Neural correlation is stimulus modulated by feedforward inhibitory circuitry
Journal of Neuroscience 32(2):506-18 (2012)
I used to be a computational neurobiologist. This paper reports some initially surprising correlations in data recorded from excitatory and inhibitory cells in the rodent sensory cortex, and develops an elegant non-linear model that explains these correlations.
A Feedback Information-Theoretic Approach to the Design of Brain-Computer Interfaces
International Journal of Human-Computer Interaction (Special Issue: Current Trends in Brain-Computer Interface (BCI) Research and Development), 27: 1, 5-23 (2011)
As an undergraduate, I studied and built brain-computer interfaces (BCIs). This paper shows how to design an information-theoretically optimal brain-computer interface, and reports the results of some of our experiments with an EEG-based BCI.