[CSE 130] Programming Languages: Principles and Paradigms (Winter 2014)
[Summer Academy in Applied Science & Technology] Computer Science (2007)
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.
[POPL 2012, OOPSLA 2012]
- Staged Information Flow (SIF) [PLDI 2009]
- 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.