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

    Faculty

  • Adam Chlipala

    • Postdocs

  • Duckki Oe
  • Antonis Stampoulis

    • PhD students

  • Gregory Malecha
  • Peng Wang

    • Master's students

  • Drew Haven

    • Undergrads

  • Benjamin Barenblat
  • Jason Gross
  • Patrick Hurst
  • Michael Kelessoglou
  • Tony Zhao

    • Others

  • Santiago Cuellar

    • Collaborators

  • David Spivak

    • Past members