Research interests (Summary)
    I study programming languages and computer security. Most recently, my work has focused on two research directions: (1) language-based enforcement of information-flow policies and understanding dynamic security policies, and (2) access control and authorization logic. I am also interested in secure concurrent and distributed computing, functional programming languages, type theory, linear and modal logics, theorem proving and mechanized metatheory. More information about my research can be found in this research statement.

Research Activities, News, and Conferences
    :: New! Computer Security Foundations (CSF) 2011
    :: POPL 2011
    :: NoBot: Networks Opposing Botnets
    :: SoftBound
    :: Manifest Security
    :: Security Oriented Languages (SOL)
    :: Penn's PL Club
    :: New Jersey Programming Languages Seminar (NJPLS)

Recent Publications (Complete List)
    - Generative Type Abstraction and Type-level Computation [POPL 2011]
    - Relational Parametricity for Polymorphic Linear Lambda Calculus [APLAS 2010]
    - Lolliproc: to Concurrency from Classical Linear Logic via Curry-Howard and Control [ICFP 2010]
    - CETS: Compiler-Enforced Temporal Safety for C [ISMM 2010]
    - Lightweight Linear F [TLDI 2010]
    - Reactive Noninterference [CCS 2009]
    - Encoding Information Flow in AURA [PLAS 2009]
    - Updatable Security Views [CSF 2009]
    - SoftBound: Highly Compatible and Complete Spatial Memory Safety for C [PLDI 2009]
    - «more»

Current Ph.D. Students and Post Docs
    > Karl Mazurak (Linear languages and protocols)
    > Peter-Michael Osera (Language interoperability)
    > Qi (Aileen) Zhang (Program Synthesis)
    > Jianzhou Zhao (LLVM in Coq, SoftBound, Mechanized Metatheory)

Former Ph.D. Students and Post Docs
    . Jeff Vaughan (Ph.D. 2009, now a post doc at UCLA)
    . Limin Jia, Ph.D. (post doc 2007-2009, now at CMU)
    . Peng Li (Ph.D. 2008, now at Google)
    . Stephen Tse (Ph.D. 2007, now at a startup)

Former Undergraduate Students
    . Luke Zarko (2009)
    . Roman Shor (2008)
    . Joey Schorr (2008)
    . Matt Gruskin (2008)
    . Dan Margolis (2006)
    . Kate Moore (2004)

Teaching (Summary)
    * CIS 120: [2010]
    * CIS 341: Compilers [2008]
    * CIS 700: Software and Compiler Verification [2005]
    * CIS/TCOM 551: Computer and Network Security [2009] [2008] [2007] [2006] [2005]
    * CSE 331: Introduction to Networks and Security [2006] [2004] [2003] [2002]
    * CIS 700: π -Calculus and Foundations of Concurrent Systems [2004]
    * CIS 670: Advanced Topics in PL (Safety and Security) [2003]

Awards and Honors
    - Alfred P. Sloan Fellow, 2009-2010
    - NSF CAREER award, 2004
    - Best Paper award at SOSP, 2001
    - Intel Foundation Graduate Fellowship, 2001
    - Best Paper award at ICFP, 1999
    - NSF Graduate Student Fellowship, 1996

Funding
My research has been supported in part by the following grants. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
    - NSF 0311204: Dynamic Security Policies
    - NSF 0346939: CAREER: Language-based Distributed System Security
    - NSF 0524059: Resource-guided Implementation of Secure Embedded Software
    - NSF 0524035: Flexible, Decentralized Infomation-flow Control for Dynamic Environments
    - NSF 0551589: CRI: Machine Assistance for Programming Language Research
    - NSF 0541040: CCF: Unifying Events and Threads: Language Support for Network Services
    - NSF 0716469: CT-T: Collaborative Research: Manifest Security
    - ONR: TIME-DC

[Curriculum Vita]     [Talks]     [Writing Tips]