Lectures given at Purdue University, January 2009.
Part of the CS 565: Programming Languages course, held by Suresh Jagannathan and Jan Vitek.
The Coq Proof Assistant can be downloaded from here. The files of these lectures should be compatible have been tested with version 8.1pl3 but should work with any 8.1 (or later) version.Be sure to install also the CoqIde graphical interface (recommended). If you are familiar with Emacs, you may want to run Coq inside Proof General instead.
Documentation can be found here.
- Source file for the first lecture: Coq as a programming language.
- Source file for the second lecture: Coq for logical reasoning.
Disclaimer: working with Coq (more in general, working with proof assistants) can be extremely frustrating. If you are stuck on one exercise, do not hesitate to contact me and ask for help.
Email: Francesco.Zappa_Nardelli (at) inria.fr
Address: Francesco Zappa Nardelli, Projet Moscova, INRIA Paris-Rocquencourt, Domaine de Voluceau, B.P. 105, 78153 Le Chesnay Cedex, France