Research interests

It is too hard to build trustworthy software systems. I aim for simple, high-level abstractions that offer programmers strong guarantees about cross-cutting concerns: security, distribution, extensibility, persistence.

Selected recent publications

An abstract yet expressive model for reasoning robustly about the interaction between authorization and information flow.

Effective localization of type errors in the rich type system of Haskell. (Distinguished paper award)

An expressive, lightweight genericity mechanism with better code reuse and stronger static checking

LALR parsers can illustrate parsing conflicts with counterexamples

SecVerilog: a security-typed hardware design language for building hardware without leaks or timing channels

Current Projects

[Show courses taught]