There is a strong correspondence between mathematics and programming, under which mathematical proofs correspond to programs. A proof assistant is a tool that a mathematician/programmer can use to represent proofs/programs, in such a way that a computer can verify whether or not they are correct. The use of proof assistants in math and computer science is becoming ever more important for managing the increasing complexity of proofs and programs. Proof assistants have been used to check significant mathematical theorems, such as the Four Color Theorem and the Feit-Thompson Odd-Order Theorem, as well as large pieces of software, such as a C compiler and the definition of the Standard ML programming language.
In this course, you will learn to use a proof assistant to write computer-checked programs and proofs. Specifically, you will use the Agda proof assistant to verify functional and imperative programs, and to formalize mathematics in Homotopy Type Theory. More broadly, on the computer science side, you will improve your ability to reason about your code. On the math side, you will learn how to do mathematics based on type theory instead of set theory, and you will understand the advantages and challenges of this approach.
Prerequisites: COMP 212 (CS II), or permission of instructor. Students without knowledge of functional programming (as is often taught in CS II) or programming languages (as in COMP 321) may need to do some extra background reading.
There will be two course meetings per week. This time will be used for chalk-board lectures, for interactively coding as a whole class, and for small-group or individual work. Because the material covered in this class is cutting-edge research, there are no comprehensive written sources, and the material that we develop during lecture will be your primary resource. Which is to say: attendance is strongly encouraged. In the first half of the semester, you will complete five weekly homework assignments, followed by a take-home exam. In the second half, there will be additional homeworks (possibly 2-weeks each), and a final project.