Associate Professor without Tenure of Computer Science
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 the current "master plan" in the group, which may be useful for people considering applying for student or postdoc positions.
|Bedrock, a new foundation for an ecosystem of software development tools running entirely inside of Coq, supporting multilanguage programming of systems with assembly-level correctness proofs|
|Fiat, a Coq framework for refining specifications into efficient programs|
|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.|