News

  1. [Jun 2016] Sketch-n-Sketch presented by Brian at PLDI 2016.
  2. [May 2016] Prodirect Manipulation presented at ICSE 2016.
  3. [Feb 2016] Sketch-n-Sketch appears on Elm page, Lambda the Ultimate, and Hacker News.

... More News ...

Currently Teaching

None (Summer 2016)

... More Classes ...

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. Below are some of the projects I've worked on. For more information about my research, check out my publications and talks.


active projects

 
[Sketch-n-Sketch] Direct manipulation interfaces are useful in many domains, but the lack of programmability in a high-level language makes it difficult to develop complex and reusable content. We present a prodirect manipulation editor for scalable vector graphics (SVG), which allows the user to freely mix between programmatic and direct manipulation.
 
[Dependent JavaScript] 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.

older projects

 
[Radar] 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] 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.

Students

Brian Hempel (PhD student)
Amy Sitwala (BS student)
Bowen Wang (BS student)
John Zhao (BS student)

Jacob Albers (BS 2016)
Mitchell Spradlin (BS 2016)
Izaak Meckler (BS 2015, Honors Thesis)

Professional Activities

2017: PLDI PC
2016: POPL SRC, PLDI ERC, ECOOP PC, TFP PC, Midwest PL Summit (Co-organizer)
2015: POPL PC, PLDI SRC, STOP PC, OOPSLA ERC
2014: PLDI ERC, PLDI AEC, OOPSLA PC
2013: FOOL PC