This directory provides supporting materials for the talk by Mihir Mehta in the ACL2 Seminar, 12/2/2016 and 12/9/2016.

Abstract:
Mihir Mehta will give an introduction to the Coq prover, with a focus on induction proofs and modeling programming languages.

The gzipped tar file spec.tar.gz extracts to subdirectory spec/:

• Part 1 is IndProp.v
• Part 2 is Imp.v
• Part 3 is Tactics.v

Credit is owed to Benjamin Pierce of the University of Pennsylvania for the online book, titled Software Foundations, that provides much of the material for this talk and some of the proofs.