A Programming Language for Secure Web and Mobile Development. We are currently designing a new programming language called Wyvern that is designed to help in developing highly secure web and mobile applications, while at the same time enhancing developer productivity. Research on this project includes a novel object model and versioned module system that provides a foundation for security, and an extensible language and type system, which supports domain-specific languages for UI layouts, distributed application architectures, and security policies. Lightweight Formal Methods show great promise for helping software engineers write secure software, avoid defects, and achieve high parallel performance and other non-functional goals. I am interested in how language and type system design can be used to more effectively check a range of critical software properties. We are currently developing an approach, for example, that provides a simple typed interface to a parallel library, while using more sophisticated formal methods to prove that subtle concurrency tricks used in the library are correct. This approach may thus be able to provide both high usability and high performance—an elusive combination in past work. More broadly, I am interested in using formal abstractions that capture engineers’ informal reasoning, especially in the presence of challenges such as concurrency and mutable aliased state.