Introduction to the Coq Proof Assistant

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.