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, the Kepler conjecture, 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 programs. More broadly, you will improve your ability to program and prove at the same time.
Prerequisites: COMP 212 (CS II), or permission of instructor.
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. In the second half, there will be additional homeworks (possibly 2-weeks each).