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
  • Fiat, deriving programs automatically from specifications in Coq
  • Ur/Web, a domain-specific functional programming language for Web applications, inspired by dependent types
  • Kami, a framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components
  • For More Information

    For a list of group members, publications, etc., see Adam Chlipala's home page.