Adam Chlipala Associate Professor of Computer Science Programming Languages & Verification Group (more PL at MIT) Computer Science and Artificial Intelligence Laboratory Department of Electrical Engineering and Computer Science MIT Email: adamc@csail.mit.edu Office: 32G842 
I'm in a transitional period, in terms of simple descriptions of my research interests. My traditional areas are programming languages and formal methods, but my interests have broadened to include other aspects of computersystem design and implementation. I like the idea of doing cleanslate redesign of computing stacks with current security and privacy concerns frontandcenter, which I do believe involves, in a central way, my traditional focus of mechanized mathematical proofs, especially with the Coq proof assistant. However, I also spend a fair amount of time now thinking more generally about pleasant interfaces (e.g., hardware instruction sets, OS systemcall interfaces, programming languages) and efficient implementations of hardware and software systems, including through tinkering with traditional boundaries between layers.
I try to organize my research group as something like a startup company looking to produce one convincing unified demo of a cleanslateish fullstack, practical computer system. (Like startup companies, we expect to pivot often based on what we learn!) We are looking at simple embedded applications now, where the scope of machinechecked proofs and unified interface redesign reaches from RTL to relational specifications of network protocols. I'm interested in recruiting students to contribute. I do sometimes hire postdocs, though most of my recruiting strategy is centered on students (PhD, master's, undergrad). Ideal candidates have strong backgrounds in both rigorous mathematical reasoning and software/hardware systems implementation. There tends to be a bad match with students who use the word "theory" to describe their interests within programming languages or formal methods, to the point where our PhD program generally won't admit those people (they'd be betterserved elsewhere!). Current MIT students interested in working together should email me, while for others I suggest following our normal PhD application process.
For a bit more info on what I work on, two lowtimeinvestment overviews (of the mechanizedproofs part) are my blog post on the surprising security benefits of formal proofs and video of a talk I gave at the 34th Chaos Communication Congress in December 2017.
needs logo  Unnamed (and somewhat incipient) umbrella project to build demonstration software/hardware systems with endtoend mechanized proofs. I started my time as faculty developing the Bedrock library for verified multilanguage programming, but that project is largely over; we are working on a replacement project now that shares the name but makes very different design decisions, still supporting separationlogicverified lowlevel programs (in a tasteful language, not C!) processed by a verified compiler, which I would like to use to explore alternative and drastically simplified OSlike functionality. The programming layer on top is meant to involve our Fiat system for automatic and correctbyconstruction program derivation from specifications, which we are currently experimenting with using to generate code for practical network servers, a convenient domain for trying to make highlevel programming more like relationaldatabase programming but without the usual rough edges. Beneath the level of assembly language, we have work in the Kami project on modular hardware verification and verified compilation, where development is proceeding now jointly with industry, and where I'm especially interested in exploring alternative concurrency support in generalpurpose processors. One of the crosscutting focuses now is cryptography, including in our Fiat Cryptography project that centers on what is essentially a verified domainspecific compiler for finitefield arithmetic, which should soon be included in the build process for Google Chrome (to produce some of the code to validate SSL connections). 
FSCQ, a file system verified in Coq using a separation logic for reasoning about crash safety, mostly carried out these days by colleagues in the PDOS group  
The Science of Deep Specification, a National Science Foundation Expedition in Computing, 20162021, promoting similar fullstackverification research to what I described above, but on more conventional architectures 
Ur/Web, a domainspecific functional programming language for modern Web applications. I started working on it when I was a grad student, and it's pretty much done researchwise, yielding a productionquality tool suite that a fair number of people enjoy using.  
Lambda Tamer, an umbrella library for the experiments in compiler verification that I started as a grad student. The most concrete outcome of the work was the parametric higherorder abstract syntax (PHOAS) encoding of program syntax, which we still put to use in many of my projects, where different kinds of compilers remain frequent ingredients in novel system designs. 
(An "*" indicates a class I [co]created.)
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant An introduction to the Coq proof assistant, assuming just familiarity with rigorous math and functional programming. Presents the techniques needed to scale to large formal developments in program verification and other domains, including scripted proof automation and expressive types for embedded programs. 

FRAP 
Formal Reasoning About Programs Introducing Coq simultaneously with semantics and program proof methods. Emphasizes commonalities through casting (almost) everything in terms of invariants on transition systems, with abstraction and modularity as our standard tools for simplifying invariant proofs. Presents ideas in parallel as chapters of a PDF with standard math notation and in Coq source files, mixing in bits of proofautomation wizardry at the author's whim. [I've used this book so far in three iterations of a graduate class and plan to finetune it through at least one more offering before declaring it betaquality; but, for intrepid instructors of related classes, it could be worth experimenting with already!] 
I'm straying pretty offtopic here, but, especially for all the students who might be reading this far down the page, I'd like to recommend a few books that have had big influences on me and that I wish I'd been told about as a student.