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

    Faculty

  • Adam Chlipala
  • Postdocs

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

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

  • Benjamin Barenblat
  • Stephan Boyer
  • Undergraduates

  • Samuel Duchovni
  • William Navarre
  • Ziv Scully
  • Other

  • Thomas Grégoire
  • Mutaamba Maasha
  • Collaborators

  • David Spivak
  • Past members