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
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
For More Information
For a list of group members, publications, etc., see Adam Chlipala's home page.