My research interests are best described by considering the sorts of problems and solutions that I enjoy.
When I write software, I like to be lazy, letting the computer check that I'm not making certain kinds of mistakes. Formal logic is the best tool I know to provide the strongest guarantees about absence of important classes of mistakes. Especially when it comes to computer system security, the economic value of formal guarantees seems very compelling to me. However, software development practitioners are generally skeptical about the real-world applicability of logic because the most well-known solutions impose intractable costs on the programmer. I agree that the formal methods world has more often than not produced tools that cost too much to use. One recurring theme in my research is reducing the human cost of achieving rigorous logical guarantees, via different approaches for structuring programs and logical developments and then automating large parts of the associated proofs. Here I'm talking about formal proofs, which are especially rigorous versions of mathematical proofs that are more familiar to the average computer scientist. The game is all about getting every detail right, and computers are very good at that sort of thing, so my research aims to take advantage of algorithmic support in proof construction.
The word "theory" shows up a lot in the names of techniques that I apply in my research, but I'm motivated by practical considerations. Generally I try to be working on projects with mixed time horizons for improving the lives of real programmers and consumers, ranging between about 2 to 10 years to turn research ideas into production systems. Some of my work in programming language design is already being used in production systems and commercial development, while work using interactive theorem proving is more experimental, though I hope to construct some practical systems with it in the next few years!
All the work I do is related to functional programming, and there are a few simple questions you can ask yourself to get a sense for how well our research tastes align.
Generally, I will be looking for collaborators who are enthusiastic about one or both of the above topics, and who have top-notch track records in doing related research. I may also consider candidates who are interested but inexperienced in these specific topics, when they have substantial experience in software development (though a purely theoretical background is unlikely to be a good match). Feel free to contact me if you have questions about what we could work together on.
Languages of this sort rule out the most common Web application security bugs by construction. Compared to related language efforts, Ur/Web also has a number of novel capabilities:
Further, Ur/Web is developed as a practical programming tool, not just a research prototype. See the project site for pointers to real applications under development with Ur/Web.
A variety of exciting projects today are carrying out machine-checked proofs of strong correctness properties for complete software stacks, from operating systems and compilers on up. The human cost of building these proofs has been high. Some projects prove weaker properties (like type safety, rather than functional correctness) but do so with much cheaper, mostly automated proofs. I am interested in getting the best of both worlds: proving strong theorems about all software layers of a system, while constructing those proofs mostly through smart and sound automation. I want such proofs to be foundational, meaning that believing them depends only on a relatively small proof checking program and formalization of the semantics of a real processor instruction set.
The eventual goal here is to build complete computing platforms whose designs are based on integrated formal verification. This should make it possible to avoid depending on expensive run-time checks in hardware and software (e.g., virtual memory protection) to enforce process isolation and security policies. At the same time, we may produce stronger application correctness guarantees than are possible with current systems. I plan to investigate applying this technology to server/cloud, desktop, mobile, and embedded applications, ideally through a common set of theoretical and practical tools.
Work so far has concentrated on the Bedrock library for Coq, which can be seen through at least two different lenses:
Many of these tasks are already being studied in great work by other groups worldwide. My focus is on not just carrying out the verifications, but on demonstrating the engineering tools that reduce programmer effort by as much as possible. (My past work in verification of compilers [papers: 1, 2, 3] and data structures [papers: 1, 2] has shown orders-of-magnitude improvements in various measures of formal proof size/effort.)
It is quite challenging to build implementations of languages with very expressive type systems, if both the compiler and the code it generates must have good performance. Based on my experience implementing Ur/Web, I've decided that implementors of these languages need better tool support. As yacc has done for parser implementation, we need tools that simplify the tasks of implementing type inference and optimization algorithms that depend on complex algebraic manipulations. (For instance, the Ur/Web type inference engine reasons about compile-time computation over database schemas, and the optimizer uses the semantics of SQL access and HTML page generation to generate tight code.)
I would like to find some collaborators interested both in building these new compiler-writing tools and in using them to experiment rapidly with designs for the next generation of functional languages in the tradition of ML and Haskell, with aspects of dependent type theory added in.
At the same time, I think we as programming language designers should be looking even further ahead to the language abstractions of the future. Functional programming takes a step beyond imperative languages in making programming more like mathematics, correspondingly improving the programmer's ability to reason about programs. How can we push this process even further, thanks to smart extensible compilers that take advantage of formal verification to let programmers teach compilers new domain-specific tricks without any risk of unsound compilation?
I think SQL is a tremendous success story for high-level declarative languages. However, the SQL model involves a language designer who works hard to pack in all the features that programmers might want, and even then it is often hard to reason about the performance of SQL queries. I would like to explore how we might implement a system that generalizes both SQL and SMT solvers, where programmers write code "directly in math," and the behavior of a program depends only on that math. Separately, the compiler (which is something like an SQL query planner) is extended with libraries of implementation strategies that have been verified to be sound using Coq. Interesting research questions here include which features are appropriate in the surface language, what the "API" for implementation strategies ought to look like, how such strategies ought to be composed, and which verification techniques will work best for showing strategy soundness.
Formal reasoning about the syntax of programming languages with nested variable binders has turned out to be a lot more complicated than most people would have guessed! I've spent some time developing approaches to the problem in the context of compiler verification, and I don't feel we yet have fully satisfactory answers to the key questions. I'm interested in working on new Coq libraries embodying novel approaches to encoding the syntax and semantics of programming languages.
I'm interested in applying computer theorem proving to homework assignments in university classes, to teach both mathematics and programming and reasoning about programs. I have some students building Coq libraries to simplify sorts of proofs that come up in a first class on discrete math and logic, and I hope to eventually apply these tools in a complete course. Ideally the class will be online as part of MITx, where it will be especially important to have automated grading of student-written proofs, since some online classes have seen hundreds of thousands of students enroll!
I'll consider advising strongly self-motivated students interested in doing other work that falls within my general interests, or even a little outside them.