# abstract

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.