Research
I enjoy developing and deploying
programming language technology
— type systems, synthesis algorithms,
and other program analysis techniques —
for applications in software engineering
and human-computer interaction.
Currently, the overarching theme of my research
is to develop
Direct Manipulation Programming Systems.
active projects
| | |
 |
[Sketch-n-Sketch]
Graphical user interfaces are great, but the lack of
programmability in a high-level language makes it difficult to develop
complex and reusable content. Sketch-n-Sketch is a
direct manipulation programming system
for interactively creating documents
(such as graphic designs, web pages, and spreadsheets)
that aims for a seamless combination of programming and direct manipulation.
|
| |
 |
[Deuce]
Text editors are great, but coding involves tedious,
error-prone edits that hinder productivity and creativity.
Deuce is a structure-aware code editor that provides direct manipulation
interactions for quickly and correctly performing several common
programming and refactoring tasks.
|
| |
 |
[Hazel with CU Boulder and CMU]
Programming environments typically provide little help when,
arguably, programmers need it the most: when editing incomplete
(syntactically ill-formed or ill-typed) programs.
This project develops semantic foundations for programming environments
to edit, run, and reason about programs with holes.
|
older projects
| |
 |
[Dependent JavaScript @ UCSD]
Scripting languages include features that frustrate
static reasoning, such as extensible objects, dynamically computed
keys, loosely coupled recursion, reflection, and dynamic code loading.
This project aims to develop type systems to
describe idiomatic programs in scripting languages
such as JavaScript, Python, and Ruby.
|
| |
 |
[Radar @ UCSD]
Defining a dataflow analysis for concurrent programs is complicated
by the subtleties of thread interleavings and locking protocols.
Radar automatically converts a sequential dataflow analysis to a
concurrent one by making use of datarace information from the
Relay race detector for C programs.
|
| | |
 |
[Staged Information Flow @ UCSD]
The prevalence of dynamically loaded code makes program analysis for
JavaScript difficult.
We present a staged approach to tracking information flow that splits the
analysis burden between compile-time and run-time.
|
| |
 |
[Fine @ Microsoft Research]
Modern SMT solvers allow refinement type systems to track security
and other complex properties, but they become a large part of the
compiler's trusted computing base (TCB). Fine incorporates a type-preserving
translation to eliminate the solver from the TCB.
Fine is a precursor to MSR's
F* language.
|
Ryerson Hall, Room 260
