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
  • 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

  • Benjamin Delaware
  • Antonis Stampoulis
  • PhD students

  • Jason Gross
  • Gregory Malecha
  • Peng Wang
  • Master's students

  • Stephan Boyer
  • Patrick Hurst
  • Undergraduates

  • Jan Polasek
  • Ziv Scully
  • Collaborators

  • David Spivak
  • Past members