My MGS course this year introduces COQ as a tool for proof formalisation.

- The COQ homepage
- Slides (updated 17/4/08)
- COQ file from 1st lecture
- 1st set of exercises
- COQ file from 2nd lecture
- 2nd set of exercises
- COQ file from 3rd lecture
- 3rd set of exercises
- COQ file from 4th lecture
- 4th set of exercises

Last modified: Fri Apr 18 09:43:46 BST 2008