MIT Programming Languages & Verification Group

Mission: 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

Current Projects

  • Bedrock, a platform for practical verification of low-level software in Coq
  • Ur/Web, a domain-specific functional programming language for Web applications, inspired by dependent types
  • Galactic, an Ur/Web course management system
  • Developing course materials to teach discrete math and logic with Coq
  • Reasoning about databases in Coq using category theory
  • Current Group Members


  • Adam Chlipala
  • Postdocs

  • C.J. Bell
  • Benjamin Delaware
  • Mohsen Lesani
  • PhD students

  • Jason Gross
  • Anders Kaseorg
  • Clément Pit--Claudel
  • Peng Wang
  • Master's students

  • Benjamin Barenblat
  • Undergraduates

  • Ziv Scully
  • Sorawit Suriyakarn
  • Other

  • Mutaamba Maasha
  • Past members