Computer Theorem-Proving for Undergrad CS Education

We are building web-based software to teach courses centered on mathematical proofs. The idea is to build an IDE usable by MIT freshmen, where it is possible to state and prove mathematical theorems, such that the system catches logical errors, much in the way that a programming IDE catches syntax or type errors. Our backend is the Coq proof assistant software, which is based on functional programming; but we want to build something much more accessible to newcomers than the common Coq interfaces. There are many opportunities to work on the general infrastructure (which is implemented in the Ur/Web language) or its application to particular course modules.

Contact Adam Chlipala at adamc@csail.mit.edu for more information.