recent news

  1. [Dec] Invited to serve on PLDI 2014 Artifact Evaluation Committee
  2. [Sep] Invited to serve on OOPSLA 2014 and POPL 2015 PCs
  3. [Sep] Presented A Fix for Dynamic Scope at ML
  4. [Sep] Defended my dissertation!
  5. [Aug] Invited to serve on PLDI 2014 ERC
  6. [May] Consider submitting a paper to FOOL 2013
  7. [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.