My research concerns the theory, design, and implementation of modern programming language features and formal verification techniques. My recent work focuses on using formal methods to investigate the (in)security of distributed applications such as cryptographic protocols.