recent news

  1. [Jun 2014] Spoke about Late Types at Dagstuhl
  2. [May 2014] Spoke at Pint of Science US in San Diego
  3. [May 2014] Excited to join the faculty at The University of Chicago this fall!
  4. [Dec 2013] Invited to serve on PLDI 2014 Artifact Evaluation Committee
  5. [Sep 2013] Invited to serve on OOPSLA 2014 and POPL 2015 PCs
  6. [Sep 2013] Presented A Fix for Dynamic Scope at ML
  7. [Sep 2013] Defended my dissertation!
  8. [Aug 2013] Invited to serve on PLDI 2014 ERC
  9. [May 2013] Consider submitting a paper to FOOL 2013
  10. [May 2013] Presented Dependent JavaScript at HCSS

teaching

@UCSD
[CSE 130, Winter 2014] Programming Languages: Principles and Paradigms

@UPenn
[SAAST, Summer 2007] Computer Science (Lecture Notes)
[CSE 399, Spring 2007] C# Programming

research projects

I am interested in programming language, compiler, and program analysis technology. My thesis work targets type systems for dynamic languages. For more information about the projects below, check out my research page for publications and talks.


  • Dependent JavaScript (DJS) [POPL 2012, OOPSLA 2012]
    Dynamic languages incorporate features that are notoriously difficult for type systems to reason about. We define nested refinements to track these features in the purely functional System D calculus, and we scale up the approach to the imperative, prototype-based JavaScript setting.
  • Staged Information Flow (SIF) [PLDI 2009]
    JavaScript security is increasingly important, but the prevalence of dynamically loaded code makes program analysis difficult. We present a staged approach to tracking information flow that splits the analysis burden between compile-time and run-time.
  • Fine [ESOP 2010, PLDI 2010]
    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). We build a type-preserving translation that eliminates the solver from the TCB by converting SMT reasoning directly to the programming language in proof-carrying style.
  • Radar [PLDI 2008]
    Defining a dataflow analysis for concurrent programs is complicated by the subleties of thread interleavings and locking protocols. We present an automatic conversion from a sequential dataflow analysis to a concurrent one by making use of datarace information.