Assistant Professor of Electrical Engineering and Computer Science
Douglas T. Ross (1954) Career Development Professor of Software Technology
Programming Languages & Verification Group (more PL at MIT)
Computer Science and Artificial Intelligence Laboratory
Department of Electrical Engineering and Computer Science
Interested in joining my research group (at any level: undergrad, masters, PhD, postdoc; already admitted or considering applying)? Please drop me a line to discuss any specific ideas you have for collaboration on projects in programming languages or formal verification!
I've also written a summary of my research interests and projects, which may be useful for people considering applying for student or postdoc positions.
|Bedrock, a new low-level programming language, embedded within Coq, with support for mostly-automated verification of functional correctness. My goal is to use Bedrock to implement a complete verified software stack that can rely on static verification to take over from uses of dynamic techniques for enforcing process isolation.|
|Ur/Web, a domain-specific functional programming language for modern Web applications, inspired by dependent type systems. Supports strong encapsulation of key Web application resources, statically-typed metaprogramming, and static analysis for conformance to declarative security policies. Not just a research prototype! Has a growing programmer community and some commercial application development underway.|