MIT Programming Languages & Verification Group

Improve the software development process by replacing ugly development techniques with beautiful ones.
Secret weapon
Applied mathematical logic, including computer theorem proving (especially Coq) and type systems.
Visit us on GitHub.
Latest news
See our blog and our CSAIL page.
Group members, publications, etc.
See Adam Chlipala's home page.