Theorem Proving

This course explores computer-assisted theorem proving with the Coq Proof Assistant. The course will teach students to formally specify software and model mathematical theories. We will then study techniques for mechanically proving theorems about these Coq. Prerequisites: CSCI 1730 or CSCI 0170 and permission of the instructor.