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, and the Liquid Tensor Experiment, as well as large pieces of software, such as a C compiler, cryptographic primitives used in web browsers, 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 (so please bring your laptop every class). 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. There will be 8 to 10 homeworks over the course of the semester. The topics for later homeworks may vary according to the interests of the class.
Your grade will be based on homework assignments (70%), participation in the in-class exercises/labs (10%), and a 1-on-1 oral exam / final homework presentation during exam week (20%).