| INTRODUCTION TO THE UNIVALENT FOUNDATIONS OF MATHEMATICS/COMPUTER SCIENCE AND DISCRETE MATHEMATICS SEMINAR II | |
| Topic: | Introduction to the Coq Proof Assistant |
| Speaker: | Andrew Appel |
| Affiliation: | Princeton University |
| 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.