|INTRODUCTION TO THE UNIVALENT FOUNDATIONS OF MATHEMATICS/COMPUTER SCIENCE AND DISCRETE MATHEMATICS SEMINAR II|
|Topic:||Introduction to the Coq Proof Assistant|
|Date:||Tuesday, December 7|
|Time/Room:||11:00am - 12:00pm/S-101|
A "proof assistant" is a software package comprising a validity checker for proofs in a particular logic, accompanied by semi-decision procedures called "tactics" that assist the mathematician in filling in the easy parts of the proofs. I will demonstrate the use of the Coq proof assistant in doing simple proofs about inductive structures such as natural numbers, sequences, and trees.