Programming Proofs

Undergraduate / Graduate

In this course, we will explore the use of proof assistants, computer programs that allow us to write, automate, and mechanically check proofs. These tools have two main uses. They allow us to prove properties of our programs, thereby guaranteeing that our code is free of software errors. They also allow us to formalize mathematics, stating and proving mathematical theorems in a manner that leaves no doubt as to their meaning or veracity. At the intersection of these two uses lies mechanized computer science, involving proofs about data structures, algorithms, programming languages and verification itself.