6.892  Interactive Computer Theorem Proving

Interactive proof assistant software makes it possible to build mathematical proofs that can be checked algorithmically, providing a much higher level of assurance than we can hope to achieve with traditional human proof-checking.  This technology has been in development since at least the 1960's and has, around the start of the 21st century, started to achieve significant popularity in certain domains.  Applications range from high-confidence proofs of celebrated mathematical theorems like the four color theorem, to proofs that particular pieces of executable software obey their correctness specifications.

This course introduces general principles of interactive theorem proving with the proof assistant Coq, with a focus on the engineering techniques that are important for large developments, whether for complex mathematical theories or the verification of large, layered software systems.  Students will do problem sets proving some simple theorems and then carry out research projects that apply the ideas of the course.  The target audience includes people interested in formalized mathematical proofs for any domain.

Prerequisites: "mathematical maturity" and familiarity with discrete math and logic (for instance, from 6.042J), plus some programming experience

Text: online drafts of a textbook in progress, "Certified Programming with Dependent Types"

Instructor's home page