Adam Chlipala 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 MIT Email: adamc@csail.mit.edu Office: 32G842 
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. Other resources along those lines are my interview on the Functional Geekery podcast in summer 2017 and this short profile in MIT Technology Review from fall 2017.
Bedrock, a new foundation for an ecosystem of software development tools running entirely inside of Coq, supporting multilanguage programming of systems with assemblylevel correctness proofs  
Fiat, a Coq framework for refining specifications into efficient programs  
FSCQ, a file system verified in Coq using a separation logic for reasoning about crash safety  
Kami, a platform for verified hardware programming in Coq  
Ur/Web, a domainspecific 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.  
The Science of Deep Specification, a National Science Foundation Expedition in Computing, 20162021 
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 two 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!] 